Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Associative and Commutative Binary Operations, and Neutral Elements
definitiondef:operation-laws-nbg-2026bAlgebraA binary operation is associative if regrouping does not change a product of three elements, commutative if the order of two factors does not matter, and an element is neutral if combining it with any element returns that element.The Natural Numbers with Zero and Their Embedding into the Integers
lemmalem:natural-numbers-with-zero-nbg-2026aAlgebraSet TheoryThe set of natural numbers with zero is the set of natural numbers together with zero, and sending zero to the integer zero and each natural number n to the integer ι(n) gives an injective map into the integers that preserves sums, products and order, with the nonnegative integer…The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness
settingset:real-numbers-nbg-2026cAnalysisAlgebraFixes the real numbers as an ordered field with the standard notation, identifies natural numbers, integers, rationals and sets of them with their images in the reals, so that N ⊆ N_0 ⊆ Z ⊆ Q ⊆ R, and carries completeness with its consequences: infima, the Archimedean property, d…Ordered Fields in Which Every Nonempty Set Bounded Above Has a Supremum Are Unique up to Unique Isomorphism
theoremthm:least-upper-bound-ordered-field-unique-nbg-2026bAnalysisAlgebraFor any two ordered fields in which every nonempty set bounded above has a supremum, there is exactly one homomorphism of ordered fields from the first to the second; it is an isomorphism and it fixes every rational number.The Real Numbers Form an Ordered Field in Which Every Nonempty Set Bounded Above Has a Supremum
theoremthm:real-numbers-nbg-2026aAnalysisAlgebraThe real numbers form an ordered field in which every nonempty set bounded above has a supremum, and the canonical embedding of the rationals sends each rational to its rational cut.Multiplication of Dedekind Cuts: Associativity, Commutativity, Unit, Distributivity, Reciprocals and Nonnegative Products
lemmalem:dedekind-cut-multiplication-nbg-2026aAlgebraSet TheoryMultiplication of Dedekind cuts is associative, commutative and distributive over addition, has the cut of 1 as unit, gives every nonzero cut a reciprocal, keeps products of nonnegative cuts nonnegative, and multiplies rational cuts like the rationals.Addition and Order of Dedekind Cuts: an Ordered Abelian Group in Which Every Nonempty Set Bounded Above Has a Supremum
lemmalem:dedekind-cut-addition-order-nbg-2026aAlgebraSet TheoryAddition of Dedekind cuts is associative and commutative with neutral element the zero cut and inverses given by the negative; it respects inclusion; every nonempty set of cuts bounded above has its union as supremum; and rational cuts add and compare like the rationals.- The real numbers are the Dedekind cuts of the rationals, ordered by inclusion, added elementwise, and multiplied through the products of their absolute values with the sign fixed by the signs of the factors; zero and one are the cuts of the rationals 0 and 1.
Construction of the Dedekind Cuts: They Form a Set Totally Ordered by Inclusion, Closed under Sums, Negatives and Products of Nonnegative Cuts
lemmalem:dedekind-cut-construction-nbg-2026aAlgebraSet TheoryThe downward-closed proper nonempty sets of rationals without a greatest element form a set, totally ordered by inclusion; rational cuts, sums, negatives and products of nonnegative cuts are again such sets.Infima, the Archimedean Property, Density of the Rationals and Rational Approximation from Below in an Ordered Field Whose Nonempty Sets Bounded Above Have Suprema
lemmalem:least-upper-bound-ordered-field-nbg-2026bAnalysisAlgebraIn an ordered field in which every nonempty set bounded above has a supremum, nonempty sets bounded below have infima, every element lies below some natural number, the rationals are dense, and every element is the supremum of the rationals below it.The Canonical Embedding of the Rational Numbers into an Ordered Field
definitiondef:ordered-field-rational-embedding-nbg-2026aAlgebraThe canonical embedding of the rationals into an ordered field is the unique map from the rationals preserving sums, products and the unit.The Rational Numbers Embed in Exactly One Way into Every Ordered Field
lemmalem:ordered-field-rational-embedding-nbg-2026aAlgebraIn every ordered field there is exactly one map from the rationals preserving sums, products and the unit; it is an injective homomorphism of ordered fields that preserves and reflects the strict order, negatives and reciprocals.Homomorphisms and Isomorphisms of Ordered Fields
definitiondef:ordered-field-homomorphism-nbg-2026aAlgebraA homomorphism of ordered fields is a map preserving sums, products, the unit and the order; an isomorphism is a bijective homomorphism that also reflects the order.The Integers and the Rational Numbers, with the Natural Numbers and the Integers Identified with Subsets of the Rationals
settingset:rational-numbers-nbg-2026cAlgebraSet TheoryFixes the integers as an ordered ring and the rationals as an ordered field, with the standard notation, and identifies natural numbers, integers and sets of them with their images in the rationals, so that N ⊆ N_0 ⊆ Z ⊆ Q.The Natural Numbers and the Integers inside the Rational Numbers
lemmalem:rational-embedding-nbg-2026aAlgebraSet TheoryInside the rationals, the natural numbers sit via n ↦ j(ι(n)), which is injective, positive and preserves 1, sums, products and order; the negations of Z and Q are their ring negatives; and every rational [x, m] is the quotient of the integer x by the natural number m.Rules of Arithmetic and Order in an Ordered Field
lemmalem:ordered-field-rules-nbg-2026aAlgebraSet TheoryThe familiar rules in an ordered field: zero products, signs, reciprocals, adding and multiplying inequalities, squares are nonnegative and 0 < 1, reciprocals of positive elements, the midpoint of two elements lies strictly between them, and the properties of absolute value inclu…- 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 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.