Revision #2151 → #2826 · back to history
modifiedUnary addition operationec446a811e58
| Field | From #2151 | To #2826 |
|---|
| mathlib.decl | AddLeftCancelMonoid | — |
| mathlib.match_kind | generalization | — |
| mathlib.module | Mathlib.Algebra.Group.Defs | — |
| note | Mathlib uses the binary `Add` class; one-sided addition corresponds to left/right add-cancel classes but is not separately defined. | Mathlib exposes addition only as a binary operation; the one-sided "add a fixed amount" unary view is not a separate Mathlib construct. |
| status | partial | not_formalized |
modifiedSuccessor and addition as iterated succession3a275b15180d
| Field | From #2151 | To #2826 |
|---|
| mathlib.decl | AddMonoid.nsmul_succ | Nat.add_succ |
| mathlib.module | Mathlib.Algebra.Group.Defs | Init.Data.Nat.Basic |
| note | `AddMonoid.nsmul_succ : nsmul (n+1) x = nsmul n x + x` formalizes iterated addition/successor. | `Nat.add_succ : n + (m + 1) = (n + m) + 1` encodes addition as iterated succession on ℕ. |
| provenance | ai | ai-moderated |
addedOrder-of-operations priority of addition22e2cbe07568
addedAdditive group as set closed under subtraction5cc1aa534c3a
addedDistributivity forces addition commutativityf042909abe37