Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
- Defines the absolute value |x| in an ordered field as x when 0 ≤ x and −x otherwise.
Negatives, Differences, Reciprocals and Quotients
definitiondef:field-inverses-nbg-2026aAlgebraSet TheoryDefines the negative −x and the difference x − y in a commutative ring, and the reciprocal y⁻¹ and the quotient x/y for y ≠ 0 in a field.- In a commutative ring every element has exactly one additive inverse, and in a field every nonzero element has exactly one multiplicative inverse.
- Defines the first and second components p₁ and p₂ of an ordered pair p, the unique sets with p = (p₁, p₂).
- A formula for the values defines exactly one map, on a set or on a Cartesian product, and a formula in two variables defines exactly one relation on a set.
- Defines an ordered ring as a commutative ring with a total order such that adding the same element preserves the order and products of nonnegative elements are nonnegative.
The Rational Numbers Form an Archimedean Ordered Field Containing the Integers
lemmalem:rationals-nbg-2026bAlgebraSet TheoryThe rational numbers form an Archimedean ordered field whose strict order is the strict relation of its order; the integers embed into it preserving 0, 1, the operations and the order, two fractions are equal exactly when their cross products agree, and each fraction times its de…- Defines the rational numbers as the classes [x, m] of pairs of an integer and a natural number (thought of as x/m), with the sum, product, negation and order of the construction lemma, the rationals 0 and 1, and the embedding x ↦ [x, 1] of the integers.
Construction of the Rationals: Pairs of an Integer and a Natural Number up to Equal Ratios, with Sum, Product, Negation and Order
lemmalem:rational-construction-nbg-2026bAlgebraSet TheoryPairs (x, m) of an integer and a natural number, thought of as x/m, with (x, m) ≈ (y, n) when x·n = y·m, form an equivalence relation; on the classes [x, m] there are unique sum, product, negation and order given by the usual formulas.The Integers Form an Ordered Ring Containing the Natural Numbers as Its Positive Elements
lemmalem:integers-nbg-2026bAlgebraSet TheoryThe integers form an ordered commutative ring; negation behaves as expected; the embedding of N is injective and preserves 1, sums, products and the order; [a, b] = ι(a) − ι(b); every integer is positive (the image of N), zero or negative; and there are no zero divisors, so nonze…- Defines the integers as the classes [a, b] of pairs of natural numbers (thought of as a − b), with the sum, product, negation and order of the construction lemma, the integers 0 = [1, 1] and 1 = [2, 1], and the embedding n ↦ [n + 1, 1] of N.
Construction of the Integers: Pairs of Natural Numbers up to Equal Differences, with Sum, Product, Negation and Order
lemmalem:integer-construction-nbg-2026bAlgebraSet TheoryPairs (a, b) of natural numbers, thought of as a − b, with (a, b) ~ (c, d) when a + d = b + c, form an equivalence relation; on the classes [a, b] there are unique sum, product, negation and order given by the usual formulas.- Defines an ordered field as a field with a total order that makes it an ordered ring.
- Defines a field as a commutative ring with 0 ≠ 1 in which every nonzero element has a multiplicative inverse.
- Defines a commutative ring (with identity) as a set with two binary operations and two distinguished elements 0 and 1 satisfying the associative, commutative, identity, additive-inverse and distributive laws.
Compatible Operations, Maps and Relations Pass to the Quotient
lemmalem:quotient-compatible-nbg-2026aSet TheoryFor an equivalence relation on a set, a binary operation, a self-map or a relation that respects the equivalence induces exactly one binary operation, self-map or relation on the quotient acting on classes through representatives.The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion
settingset:natural-numbers-nbg-2026cSet TheoryFixes the natural numbers and the natural numbers with zero, with their arithmetic, order, digits, induction and recursion, on top of the ordinary notation for sets and maps; natural numbers are used as numbers only, never as sets.Recursion on the Natural Numbers Starting at One
corollarycor:recursion-natural-numbers-nbg-2026bSet TheoryGiven a set a, a starting value c in a and a map g from N × a to a, there is exactly one map f from N to a with f(1) = c and f(n + 1) = g(n, f(n)) for every natural number n.- The familiar laws of the natural numbers in terms of N, 1, +, · and ≤: commutativity, associativity, distributivity, cancellation, the order laws and trichotomy, a < b exactly when b = a + d, compatibility of the order with + and ·, 1 is least, nothing lies between a and a + 1, e…
- Defines multiplication on omega by recursion, with m · 0 = 0 and m · S(n) = m · n + m, shows it is a binary operation on omega, and fixes that products are formed before sums.