Revision #986 → #1679 · back to history
modifiedCommutativity of addition (informal)55fee75937b2
| Field | From #986 | To #1679 |
|---|
| note | Encoded as the `AddCommSemigroup.add_comm` field/lemma. | Encoded as the `AddCommSemigroup.add_comm` field (class declared at Defs.lean:251). |
modifiedAssociativity of addition (informal)e06c18d27e4c
| Field | From #986 | To #1679 |
|---|
| note | Encoded as the `AddSemigroup.add_assoc` field/lemma. | Encoded as the `AddSemigroup.add_assoc` field (class declared at Defs.lean:182). |
modifiedAddition of 0 leaves number unchanged64b21c3870dc
| Field | From #986 | To #1679 |
|---|
| note | `AddZeroClass.add_zero` is the identity axiom for additive monoids. | `AddZeroClass.add_zero` (class at Defs.lean:384) is the identity axiom for additive monoids. |
modifiedAddition as combining sets206526f2d2b8
| Field | From #986 | To #1679 |
|---|
| note | `Cardinal.add_def` states `#α + #β = #(α ⊕ β)`, formalizing disjoint-union cardinality. | `Cardinal.add_def : #α + #β = #(α ⊕ β)` (Defs.lean:249) formalizes disjoint-union cardinality. |
modifiedSuccessor and addition as iterated succession3a275b15180d
| Field | From #986 | To #1679 |
|---|
| note | `nsmul_succ : nsmul (n+1) x = nsmul n x + x` formalizes iterated addition of 1/successor. | `nsmul_succ : nsmul (n+1) x = nsmul n x + x` (Defs.lean:648) formalizes iterated addition of 1/successor. |
modifiedComponent-wise addition of integer pairs3d8fb80a1380
| Field | From #986 | To #1679 |
|---|
| mathlib.decl | Prod.add_def | Prod.instAdd |
modifiedAddition of fractions with same denominator5a694ce7510f
| Field | From #986 | To #1679 |
|---|
| mathlib.decl | div_add_div_same | add_div |
| note | `div_add_div_same : a/c + b/c = (a+b)/c` in any division ring. | `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. |
modifiedAddition of Cauchy sequences1f85e35e1fe8
| Field | From #986 | To #1679 |
|---|
| mathlib.decl | CauSeq.add | Real.add |
| note | ℝ is the quotient of `CauSeq ℚ abs` with pointwise addition `CauSeq.add`. | `Real.add` (irreducible_def at Basic.lean:79) implements pointwise CauSeq addition on ℝ. |
modifiedAddition of complex numbersc43ba5babb2a
| Field | From #986 | To #1679 |
|---|
| note | `Complex.add_re`/`Complex.add_im` express componentwise addition on ℂ. | `Complex.add_re`/`Complex.add_im` (Basic.lean:169,173) express componentwise addition on ℂ. |
modifiedAbelian group addition4e577d2e86ad
| Field | From #986 | To #1679 |
|---|
| note | `AddCommGroup` is Mathlib's class for abelian groups written additively. | `AddCommGroup` (Defs.lean:1275) is Mathlib's class for abelian groups written additively. |
modifiedAngle addition modulo 2π391baeb85826
| Field | From #986 | To #1679 |
|---|
| mathlib.module | Mathlib.Analysis.SpecialFunctions.Complex.Circle | Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle |
| note | `Real.Angle` is ℝ/(2π ℤ) with its additive group structure. | `Real.Angle` (Angle.lean:31) is ℝ/(2π ℤ) with its additive group structure. |
modifiedAddition in abstract algebra5f4a64791765
| Field | From #986 | To #1679 |
|---|
| note | `AddCommSemigroup` captures arbitrary associative+commutative addition operations. | `AddCommSemigroup` (Defs.lean:251) captures arbitrary associative+commutative addition operations. |
modifiedLinear combinations72a5f140af75
| Field | From #986 | To #1679 |
|---|
| note | `Finsupp.linearCombination` constructs general linear combinations as a linear map. | `Finsupp.linearCombination` (LinearCombination.lean:54) constructs general linear combinations as a linear map. |
modifiedNon-commutativity of ordinal additionf4c0410d562b
| Field | From #986 | To #1679 |
|---|
| mathlib.decl | Ordinal | Ordinal.one_add_omega0 |
| mathlib.module | Mathlib.SetTheory.Ordinal.Basic | Mathlib.SetTheory.Ordinal.Arithmetic |
| note | `Ordinal` is only an `AddMonoid`/`OrderedAddCommMonoid`-style structure without an `add_comm` instance; the explicit statement `1 + ω = ω ≠ ω + 1` exists implicitly via `Ordinal.one_add_omega0`/`omega0_add_one` but I did not locate a `not_add_comm` lemma. | `Ordinal.one_add_omega0 : 1 + ω = ω` (Arithmetic.lean:1084) gives an explicit witness of non-commutativity, but no named `¬ add_comm` lemma exists. |
modifiedCommutativity of cardinal addition3d54ed29280b
| Field | From #986 | To #1679 |
|---|
| mathlib.decl | Cardinal.instCommSemiring | Cardinal.commSemiring |
| mathlib.module | Mathlib.SetTheory.Cardinal.Basic | Mathlib.SetTheory.Cardinal.Order |
| note | `Cardinal` is a `CommSemiring`, so `add_comm` holds for cardinal sums. | `Cardinal.commSemiring : CommSemiring Cardinal` (Order.lean:218) yields `add_comm` for cardinal sums. |
modifiedCoproduct as generalization of additionf715a6ecc146
| Field | From #986 | To #1679 |
|---|
| note | Binary coproducts `X ⨿ Y` are defined in `CategoryTheory.Limits`. | Binary coproducts `X ⨿ Y` are defined in `CategoryTheory.Limits` (BinaryProducts.lean has `coprod.desc`, `coprod.map`, etc.). |
modifiedSubtraction as addition of inverse561ca32f59ac
| Field | From #986 | To #1679 |
|---|
| note | `SubNegMonoid.sub_eq_add_neg : a - b = a + -b`. | `SubNegMonoid.sub_eq_add_neg : a - b = a + -b` (Defs.lean:1006). |
modifiedExponential exchanges addition and multiplication25f98c941077
| Field | From #986 | To #1679 |
|---|
| note | `Real.exp_add` and `Complex.exp_add` give `exp (x+y) = exp x * exp y`. | `Real.exp_add` and `Complex.exp_add` give `exp (x+y) = exp x * exp y` (used pervasively, e.g. SpecialFunctions/Exp.lean:42). |
modifiedDistributivity defines a ring46eab2c4e3d7
| Field | From #986 | To #1679 |
|---|
| note | `Distrib`/`Ring` build distributivity (`left_distrib`, `right_distrib`) into the ring axioms. | `Distrib` (Ring/Defs.lean:64) builds `left_distrib`/`right_distrib` into the ring axioms. |
modifiedRight distributivity of division over additione3bbb2ac478a
| Field | From #986 | To #1679 |
|---|
| note | `add_div : (a + b) / c = a/c + b/c` in any field. | `add_div : (a + b) / c = a/c + b/c` in any division ring (Field/Basic.lean:36). |
modifiedCardinal sum equals greater of two infinite cardinals4fec564209ab
| Field | From #986 | To #1679 |
|---|
| note | `Cardinal.add_eq_max : ℵ₀ ≤ a → a + b = max a b`. | `Cardinal.add_eq_max : ℵ₀ ≤ a → a + b = max a b` (Arithmetic.lean:233). |
modifiedAddition distributes over max7da60a30d030
| Field | From #986 | To #1679 |
|---|
| mathlib.decl | add_max | max_add_add_left |
| note | `add_max`/`max_add_add_right` etc. provide distributivity of addition over `max` in ordered groups. | `max_add_add_left` / `max_add_add_right` give `a + max b c = max (a+b) (a+c)` in ordered (cancel) add monoids. |
modifiedTropical addition / multiplicationd721b5a42ff2
| Field | From #986 | To #1679 |
|---|
| note | `Tropical α` defines the tropical semiring with `min`/`max` as addition and `+` as multiplication. | `Tropical α` (Basic.lean:58) defines the tropical semiring with `min` as addition and `+` as multiplication. |
modifiedConvolution as addition of random variables26fa627b4879
| Field | From #986 | To #1679 |
|---|
| mathlib.match_kind | exact | generalization |
| note | Mathlib's `Measure.mconv` together with `IndepFun` shows the law of `X + Y` is the convolution of their laws. | `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. |
| status | formalized | partial |