Revision #1679 → #2151 · back to history
modifiedCommutativity of addition (informal)55fee75937b2
| Field | From #1679 | To #2151 |
|---|
| note | Encoded as the `AddCommSemigroup.add_comm` field (class declared at Defs.lean:251). | `add_comm : a + b = b + a` is the `AddCommSemigroup` axiom. |
modifiedAssociativity of addition (informal)e06c18d27e4c
| Field | From #1679 | To #2151 |
|---|
| note | Encoded as the `AddSemigroup.add_assoc` field (class declared at Defs.lean:182). | `add_assoc : (a + b) + c = a + (b + c)` is the `AddSemigroup` axiom. |
modifiedAdding 1 is counting / successor2f15c45d9224
| Field | From #1679 | To #2151 |
|---|
| mathlib.module | Mathlib | Init.Data.Nat.Basic |
| note | `Nat.succ_eq_add_one` states `n.succ = n + 1` (inherited from core). | `Nat.succ_eq_add_one : n.succ = n + 1` is inherited from core. |
modifiedAddition of 0 leaves number unchanged64b21c3870dc
| Field | From #1679 | To #2151 |
|---|
| note | `AddZeroClass.add_zero` (class at Defs.lean:384) is the identity axiom for additive monoids. | `add_zero : a + 0 = a` from `AddZeroClass`. |
modifiedPlus sign and equals sign notation37f987d03092
| Field | From #1679 | To #2151 |
|---|
| anchors | [{"section":"Notation and terminology","snippet":"Addition is written using the plus sign"},{"type":"math_alttext","value":"{\\displaystyle 3{\\frac {1}{2}}=3+{\\frac {1}{2}}=3.5.}"}] | — |
| note | The `+` notation is the standard `HAdd.hAdd` infix in Lean/Mathlib. | The `+` infix notation is `HAdd.hAdd` (declared in core, used throughout Mathlib). |
modifiedMixed number notation60dd82ccde19
| Field | From #1679 | To #2151 |
|---|
| anchors | [{"section":"Notation and terminology","snippet":"a whole number followed immediately by a fraction indicates the sum of the two, called a mixed number"},{"type":"math_alttext","value":"{\\displaystyle 3{\\frac {1}{2}}=3+{\\frac {1}{2}}=3.5.}"}] | — |
modifiedSummationd5332e24daec
| Field | From #1679 | To #2151 |
|---|
| anchors | [{"section":"Definition and interpretations","snippet":"An arbitrary number of addition operations is called a summation"},{"type":"math_alttext","value":"{\\displaystyle \\sum _{k=1}^{5}k^{2}=1^{2}+2^{2}+3^{2}+4^{2}+5^{2}=55.}"}] | — |
modifiedSeries (infinite summation)63d15d476026
| Field | From #1679 | To #2151 |
|---|
| anchors | [{"section":"Definition and interpretations","snippet":"An infinite summation is a delicate procedure known as a series"},{"type":"math_alttext","value":"{\\displaystyle \\sum _{k=1}^{5}k^{2}=1^{2}+2^{2}+3^{2}+4^{2}+5^{2}=55.}"}] | — |
| note | Infinite sums are `tsum` (notation `∑' i, f i`) in topological add monoids. | Infinite sums are `tsum` (notation `∑' i, f i`) in topological additive monoids. |
modifiedCapital sigma notation227b76e1c087
| Field | From #1679 | To #2151 |
|---|
| anchors | [{"section":"Definition and interpretations","snippet":"it can be expressed through capital sigma notation"},{"type":"math_alttext","value":"{\\displaystyle \\sum _{k=1}^{5}k^{2}=1^{2}+2^{2}+3^{2}+4^{2}+5^{2}=55.}"}] | — |
modifiedAddition as combining sets206526f2d2b8
| Field | From #1679 | To #2151 |
|---|
| note | `Cardinal.add_def : #α + #β = #(α ⊕ β)` (Defs.lean:249) formalizes disjoint-union cardinality. | `Cardinal.add_def : #α + #β = #(α ⊕ β)` formalizes disjoint-union cardinality. |
modifiedUnary addition operationec446a811e58
| Field | From #1679 | To #2151 |
|---|
| anchor.snippet | the operation | applying the unary operation |
| note | Mathlib uses the binary `Add` class; one-sided addition corresponds to left/right add classes but is not separately defined. | Mathlib uses the binary `Add` class; one-sided addition corresponds to left/right add-cancel classes but is not separately defined. |
| provenance | ai | ai-moderated |
modifiedCommutative law of addition3dd2e7530748
| Field | From #1679 | To #2151 |
|---|
| anchors | [{"section":"Commutativity","snippet":"Addition is commutative , meaning that one can change the order of the terms in a sum, but still get the same result."},{"type":"math_alttext","value":"{\\displaystyle a+b=b+a.}"}] | — |
| note | `AddCommSemigroup.add_comm : a + b = b + a`. | `add_comm : a + b = b + a`. |
modifiedAssociative law of addition07a2eb381f07
| Field | From #1679 | To #2151 |
|---|
| anchors | [{"section":"Associativity","snippet":"Addition is associative , which means that when three or more numbers are added together, the order of operations does not change the result."},{"type":"math_alttext","value":"{\\displaystyle (a+b)+c=a+(b+c).}"}] | — |
| note | `AddSemigroup.add_assoc : a + b + c = a + (b + c)`. | `add_assoc : (a + b) + c = a + (b + c)`. |
modifiedAdditive identity (zero)dfcc42108002
| Field | From #1679 | To #2151 |
|---|
| anchors | [{"section":"Identity element","snippet":"Adding zero to any number does not change the number."},{"type":"math_alttext","value":"{\\displaystyle a+0=0+a=a.}"}] | — |
| note | `AddZeroClass.add_zero` together with `zero_add` give zero as additive identity. | `add_zero` together with `zero_add` give zero as additive identity. |
modifiedSuccessor and addition as iterated succession3a275b15180d
| Field | From #1679 | To #2151 |
|---|
| note | `nsmul_succ : nsmul (n+1) x = nsmul n x + x` (Defs.lean:648) formalizes iterated addition of 1/successor. | `AddMonoid.nsmul_succ : nsmul (n+1) x = nsmul n x + x` formalizes iterated addition/successor. |
modifiedSuccessor example: 6 + 2 = 8bfb33ef0c89c
| Field | From #1679 | To #2151 |
|---|
| mathlib.module | Mathlib | Init.Data.Nat.Basic |
modifiedAddition requires common units985d662eb636
| Field | From #1679 | To #2151 |
|---|
| note | Mathlib has no formalization of physical units arithmetic. | Mathlib has no formalization of physical-units arithmetic. |
modifiedCarry example 59 + 271e28fe0918b8
| Field | From #1679 | To #2151 |
|---|
| anchor.snippet | in the ones in the addition of 59 + 27 is 9 + 7 = 16, and the digit 1 is the carry | the ones in the addition of 59 + 27 is 9 + 7 = 16, and the digit 1 is the carry |
| provenance | ai | ai-moderated |
modifiedBinary addition with carrying74a789c786bc
| Field | From #1679 | To #2151 |
|---|
| anchors | [{"section":"Non-decimal","snippet":"Adding two single-digit binary numbers is relatively simple, using a form of carrying"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}0+0&\\to 0\\\\0+1&\\to 1\\\\1+0&\\to 1\\\\1+1&\\to 0,\\qquad {\\text{carry 1 since }}1+1=2=0+1\\times 2^{1}\\end{aligned}}}"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}5+5&\\to 0,\\qquad {\\text{carry 1 since }}5+5=10=0+1\\times 10^{1}\\\\7+9&\\to 6,\\qquad {\\text{carry 1 since }}7+9=16=6+1\\times 10^{1}\\end{aligned}}}"}] | — |
| note | Mathlib's `Nat`/`Num` addition is defined semantically rather than as a binary-carry algorithm. | Mathlib's `Nat` addition is defined semantically rather than as a binary-carry algorithm. |
addedFloating-point addition is non-associativeee0d55635d9d
modifiedAddition by cardinality of disjoint union8a5bde68f62b
| Field | From #1679 | To #2151 |
|---|
| anchor.snippet | Let | Take two disjoint sets |
| provenance | ai | ai-moderated |
modifiedRecursive definition of addition21a31ee30973
| Field | From #1679 | To #2151 |
|---|
| mathlib.module | Mathlib | Init.Prelude |
| note | `Nat.add` is defined by primitive recursion in core Lean and reused in Mathlib. | `Nat.add` is defined by primitive recursion in core Lean and used throughout Mathlib. |
modifiedDedekind's proof of associativity/commutativity1547d90a3184
| Field | From #1679 | To #2151 |
|---|
| mathlib.module | Mathlib | Init.Data.Nat.Basic |
modifiedAddition of integers by casesdaba662d1eb9
| Field | From #1679 | To #2151 |
|---|
| mathlib.module | Mathlib | Init.Data.Int.Basic |
modifiedInteger addition: −6 + 4 = −2ebe441a2c5d9
| Field | From #1679 | To #2151 |
|---|
| mathlib.module | Mathlib | Init.Data.Int.Basic |
modifiedComponent-wise addition of integer pairs3d8fb80a1380
| Field | From #1679 | To #2151 |
|---|
| anchors | [{"section":"Integers","snippet":"The addition of ordered pairs is done component-wise"},{"type":"math_alttext","value":"{\\displaystyle (a,b)+(c,d)=(a+c,b+d).}"}] | — |
| mathlib.module | Mathlib.Algebra.Group.Prod | Mathlib.Algebra.Notation.Prod |
modifiedAddition of rational numbers1bd655e3647d
| Field | From #1679 | To #2151 |
|---|
| anchors | [{"section":"Rational numbers (fractions)","snippet":"Addition of rational numbers involves the fractions"},{"type":"math_alttext","value":"{\\displaystyle {\\frac {a}{b}}+{\\frac {c}{d}}={\\frac {ad+bc}{bd}}.}"}] | — |
| mathlib.module | Mathlib | Init.Data.Rat.Basic |
modifiedAddition of fractions with same denominator5a694ce7510f
| Field | From #1679 | To #2151 |
|---|
| anchors | [{"section":"Rational numbers (fractions)","snippet":"Addition of fractions is much simpler when the denominators are the same"},{"type":"math_alttext","value":"{\\displaystyle {\\frac {a}{c}}+{\\frac {b}{c}}={\\frac {a+b}{c}},}"}] | — |
| note | `add_div : (a + b)/c = a/c + b/c` (Field/Basic.lean:36) gives the equal-denominator sum; `div_add_div_same` exists only on ENNReal. | `add_div : (a + b)/c = a/c + b/c` gives the equal-denominator sum in any division ring. |
modifiedCommutativity and associativity of rational addition76a4a04646e5
| Field | From #1679 | To #2151 |
|---|
| mathlib.decl | Rat.add_comm | add_comm |
| mathlib.module | Mathlib | Mathlib.Algebra.Group.Defs |
| note | ℚ is a `CommRing`/`Field` instance, giving `add_comm` and `add_assoc`. | ℚ is a `CommRing`/`Field` instance, giving `add_comm` and `add_assoc` for rationals. |
modifiedAddition of Dedekind cuts494ef5045d20
| Field | From #1679 | To #2151 |
|---|
| anchors | [{"section":"Real numbers","snippet":"The sum of real numbers a and b is defined element by element"},{"type":"math_alttext","value":"{\\displaystyle a+b=\\{q+r\\mid q\\in a,r\\in b\\}.}"}] | — |
modifiedAddition of Cauchy sequences1f85e35e1fe8
| Field | From #1679 | To #2151 |
|---|
| anchors | [{"section":"Real numbers","snippet":"A real number is essentially defined to be the limit of a Cauchy sequence of rationals"},{"type":"math_alttext","value":"{\\displaystyle \\lim _{n}a_{n}+\\lim _{n}b_{n}=\\lim _{n}(a_{n}+b_{n}).}"}] | — |
| mathlib.decl | Real.add | Real.instAdd |
| note | `Real.add` (irreducible_def at Basic.lean:79) implements pointwise CauSeq addition on ℝ. | `Real.instAdd` implements pointwise CauSeq addition on ℝ. |
addedAdditive inverses on the reals5a6b06b8a8ff
modifiedAddition of complex numbersc43ba5babb2a
| Field | From #1679 | To #2151 |
|---|
| note | `Complex.add_re`/`Complex.add_im` (Basic.lean:169,173) express componentwise addition on ℂ. | `Complex.add_re`/`Complex.add_im` express componentwise addition on ℂ. |
modifiedAbelian group addition4e577d2e86ad
| Field | From #1679 | To #2151 |
|---|
| note | `AddCommGroup` (Defs.lean:1275) is Mathlib's class for abelian groups written additively. | `AddCommGroup` is Mathlib's class for abelian groups written additively. |
modifiedVector additionbe8e82b9cbf0
| Field | From #1679 | To #2151 |
|---|
| anchors | [{"section":"Linear algebra","snippet":"The sum of two vectors is obtained by adding their individual coordinates"},{"type":"math_alttext","value":"{\\displaystyle (a,b)+(c,d)=(a+c,b+d).}"}] | — |
| mathlib.module | Mathlib.Algebra.Group.Pi.Basic | Mathlib.Algebra.Notation.Pi.Defs |
modifiedMatrix addition8c575dce48ac
| Field | From #1679 | To #2151 |
|---|
| anchors | [{"section":"Linear algebra","snippet":"Matrix addition is defined for two matrices of the same dimensions."},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}\\mathbf {A} +\\mathbf {B} &={\\begin{bmatrix}a_{11}&a_{12}&\\cdots &a_{1n}\\\\a_{21}&a_{22}&\\cdots &a_{2n}\\\\\\vdots &\\vdots &\\ddots &\\vdots \\\\a_{m1}&a_{m2}&\\cdots &a_{mn}\\\\\\end{bmatrix}}+{\\begin{bmatrix}b_{11}&b_{12}&\\cdots &b_{1n}\\\\b_{21}&b_{22}&\\cdots &b_{2n}\\\\\\vdots &\\vdots &\\ddots &\\vdots \\\\b_{m1}&b_{m2}&\\cdots &b_{mn}\\\\\\end{bmatrix}}\\\\[8mu]&={\\begin{bmatrix}a_{11}+b_{11}&a_{12}+b_{12}&\\cdots &a_{1n}+b_{1n}\\\\a_{21}+b_{21}&a_{22}+b_{22}&\\cdots &a_{2n}+b_{2n}\\\\\\vdots &\\vdots &\\ddots &\\vdots \\\\a_{m1}+b_{m1}&a_{m2}+b_{m2}&\\cdots &a_{mn}+b_{mn}\\\\\\end{bmatrix}}\\\\\\end{aligned}}}"}] | — |
| mathlib.decl | Matrix.instAdd | Matrix.add_apply |
| mathlib.module | Mathlib.Data.Matrix.Basic | Mathlib.LinearAlgebra.Matrix.Defs |
| note | `Matrix m n α` inherits an entrywise `Add` instance via `Pi`. | `Matrix m n α` inherits an entrywise `Add` instance via `Pi`; `Matrix.add_apply` states `(A+B) i j = A i j + B i j`. |
modifiedModular arithmetic addition4d622e361ad0
| Field | From #1679 | To #2151 |
|---|
| mathlib.module | Mathlib.Data.ZMod.Basic | Mathlib.Data.ZMod.Defs |
modifiedIntegers modulo 2 as XOR725032308b97
| Field | From #1679 | To #2151 |
|---|
| mathlib.module | Mathlib.Data.ZMod.Basic | Mathlib.Data.ZMod.Defs |
modifiedAngle addition modulo 2π391baeb85826
| Field | From #1679 | To #2151 |
|---|
| note | `Real.Angle` (Angle.lean:31) is ℝ/(2π ℤ) with its additive group structure. | `Real.Angle` is ℝ/(2π ℤ) with its additive group structure. |
modifiedAddition in abstract algebra5f4a64791765
| Field | From #1679 | To #2151 |
|---|
| note | `AddCommSemigroup` (Defs.lean:251) captures arbitrary associative+commutative addition operations. | `AddCommSemigroup` captures arbitrary associative+commutative addition operations. |
modifiedLinear combinations72a5f140af75
| Field | From #1679 | To #2151 |
|---|
| note | `Finsupp.linearCombination` (LinearCombination.lean:54) constructs general linear combinations as a linear map. | `Finsupp.linearCombination` constructs general linear combinations as a linear map. |
modifiedNon-commutativity of ordinal additionf4c0410d562b
| Field | From #1679 | To #2151 |
|---|
| note | `Ordinal.one_add_omega0 : 1 + ω = ω` (Arithmetic.lean:1084) gives an explicit witness of non-commutativity, but no named `¬ add_comm` lemma exists. | `Ordinal.one_add_omega0 : 1 + ω = ω` provides an explicit witness of non-commutativity, but no named `¬ add_comm` lemma exists. |
modifiedCommutativity of cardinal addition3d54ed29280b
| Field | From #1679 | To #2151 |
|---|
| note | `Cardinal.commSemiring : CommSemiring Cardinal` (Order.lean:218) yields `add_comm` for cardinal sums. | `Cardinal.commSemiring : CommSemiring Cardinal` yields `add_comm` for cardinal sums. |
modifiedCoproduct as generalization of additionf715a6ecc146
| Field | From #1679 | To #2151 |
|---|
| note | Binary coproducts `X ⨿ Y` are defined in `CategoryTheory.Limits` (BinaryProducts.lean has `coprod.desc`, `coprod.map`, etc.). | Binary coproducts `X ⨿ Y` are defined as `CategoryTheory.Limits.coprod` in BinaryProducts. |
modifiedSubtraction as addition of inverse561ca32f59ac
| Field | From #1679 | To #2151 |
|---|
| note | `SubNegMonoid.sub_eq_add_neg : a - b = a + -b` (Defs.lean:1006). | `sub_eq_add_neg : a - b = a + -b` from `SubNegMonoid`. |
modifiedExponential exchanges addition and multiplication25f98c941077
| Field | From #1679 | To #2151 |
|---|
| anchors | [{"section":"Arithmetic","snippet":"In the real and complex numbers, addition and multiplication can be interchanged by the exponential function"},{"type":"math_alttext","value":"{\\displaystyle e^{a+b}=e^{a}e^{b}.}"}] | — |
| mathlib.module | Mathlib.Analysis.SpecialFunctions.Exp | Mathlib.Analysis.Complex.Exponential |
| note | `Real.exp_add` and `Complex.exp_add` give `exp (x+y) = exp x * exp y` (used pervasively, e.g. SpecialFunctions/Exp.lean:42). | `Real.exp_add` and `Complex.exp_add` give `exp (x+y) = exp x * exp y`. |
modifiedDistributivity defines a ring46eab2c4e3d7
| Field | From #1679 | To #2151 |
|---|
| note | `Distrib` (Ring/Defs.lean:64) builds `left_distrib`/`right_distrib` into the ring axioms. | `Distrib` builds `left_distrib`/`right_distrib` into the ring axioms. |
modifiedRight distributivity of division over additione3bbb2ac478a
| Field | From #1679 | To #2151 |
|---|
| note | `add_div : (a + b) / c = a/c + b/c` in any division ring (Field/Basic.lean:36). | `add_div : (a + b) / c = a/c + b/c` in any division ring. |
modifiedCardinal sum equals greater of two infinite cardinals4fec564209ab
| Field | From #1679 | To #2151 |
|---|
| anchor.snippet | if either | is an infinite cardinal number , their cardinal sum is exactly equal to the greater of the two |
| note | `Cardinal.add_eq_max : ℵ₀ ≤ a → a + b = max a b` (Arithmetic.lean:233). | `Cardinal.add_eq_max : ℵ₀ ≤ a → a + b = max a b`. |
| provenance | ai | ai-moderated |
modifiedAddition distributes over max7da60a30d030
| Field | From #1679 | To #2151 |
|---|
| anchors | [{"section":"Ordering","snippet":"addition distributes over \"max\" in the same way that multiplication distributes over addition"},{"type":"math_alttext","value":"{\\displaystyle a+\\max(b,c)=\\max(a+b,a+c).}"}] | — |
| mathlib.module | Mathlib.Algebra.Order.Group.MinMax | Mathlib.Algebra.Order.Monoid.Unbundled.MinMax |
| note | `max_add_add_left` / `max_add_add_right` give `a + max b c = max (a+b) (a+c)` in ordered (cancel) add monoids. | `max_add_add_left` (and the right-handed variant) give `a + max b c = max (a+b) (a+c)` in ordered cancel monoids. |
modifiedTropical addition / multiplicationd721b5a42ff2
| Field | From #1679 | To #2151 |
|---|
| anchors | [{"section":"Ordering","snippet":"in tropical geometry one replaces multiplication with addition and addition with maximization"},{"type":"math_alttext","value":"{\\displaystyle a+\\max(b,c)=\\max(a+b,a+c).}"}] | — |
| note | `Tropical α` (Basic.lean:58) defines the tropical semiring with `min` as addition and `+` as multiplication. | `Tropical α` defines the tropical semiring with `min` as addition and `+` as multiplication. |
modifiedTropical addition via logarithm limitf97b9fa6c491
| Field | From #1679 | To #2151 |
|---|
| anchors | [{"section":"Ordering","snippet":"tropical addition is approximately related to regular addition through the logarithm"},{"type":"math_alttext","value":"{\\displaystyle \\log(a+b)\\approx \\max(\\log a,\\log b),}"},{"type":"math_alttext","value":"{\\displaystyle \\max(a,b)=\\lim _{h\\to 0}h\\log(e^{a/h}+e^{b/h}).}"}] | — |
modifiedConvolution as addition of random variables26fa627b4879
| Field | From #1679 | To #2151 |
|---|
| note | `IndepFun` (Independence/Basic.lean:144) defines independence; the law of `X+Y` as convolution of laws is encoded via `Measure.conv` / pushforward but not as a single named lemma here. | `IndepFun` defines independence; the law of `X+Y` as convolution of laws exists via `Measure` pushforwards but not as a single named convolution-of-distributions lemma here. |