Diff — 0
Revision #1680 → #1693 · back to history
modifiedZero as empty quantityb222d50591fb
| Field | From #1680 | To #1693 |
|---|
| mathlib.module | Mathlib.Algebra.Group.Defs | Init.Prelude |
| note | Mathlib has the `Zero` typeclass providing a distinguished `0`, but the informal 'empty quantity' semantics is not itself a theorem. | Mathlib/Lean has the `Zero` typeclass providing a distinguished `0`, but the informal 'empty quantity' semantics is not itself a theorem. |
modifiedMultiplication by zero58ab1eb10064
| Field | From #1680 | To #1693 |
|---|
| mathlib.decl | mul_zero | MulZeroClass.mul_zero |
| note | `mul_zero`/`zero_mul` from `MulZeroClass` give `a * 0 = 0` and `0 * a = 0`. | `MulZeroClass.mul_zero`/`MulZeroClass.zero_mul` give `a * 0 = 0` and `0 * a = 0`. |
modifiedZero smallest nonnegative integer7df67cb3f396
| Field | From #1680 | To #1693 |
|---|
| mathlib.module | Mathlib.Data.Nat.Defs | Init.Prelude |
modifiedSuccessor of zero1966fb728e66
| Field | From #1680 | To #1693 |
|---|
| note | Holds definitionally since `1` is defined as `Nat.succ 0`, but there is no dedicated named lemma. | Holds definitionally since `1` is defined as `Nat.succ 0`, but there is no dedicated named lemma — status downgraded to partial to reflect the absence of a citable declaration. |
| provenance | ai | ai-moderated |
| status | formalized | partial |
modifiedZero is evend33caeab2551
| Field | From #1680 | To #1693 |
|---|
| note | `Even.zero : Even (0 : α)` (auto-generated from `IsSquare.one` via `@[to_additive]`) states that zero is even. | `Even.zero : Even (0 : α)` states that zero is even. |
modifiedSubtraction with zeroedced1cd07e0
| Field | From #1680 | To #1693 |
|---|
| note | `sub_zero : a - 0 = a` and `zero_sub : 0 - a = -a` hold in any subtraction monoid. | `sub_zero : a - 0 = a` (with `zero_sub : 0 - a = -a`) holds in any subtraction monoid. |
modifiedMultiplication by zero rule48295336dd49
| Field | From #1680 | To #1693 |
|---|
| mathlib.decl | mul_zero | MulZeroClass.mul_zero |
| note | `mul_zero`/`zero_mul` give the multiplication-by-zero rule in any `MulZeroClass`. | `MulZeroClass.mul_zero`/`MulZeroClass.zero_mul` give the multiplication-by-zero rule in any `MulZeroClass`. |
modifiedDivision involving zero3ba18e99b77c
| Field | From #1680 | To #1693 |
|---|
| mathlib.module | Mathlib.Algebra.GroupWithZero.Basic | Mathlib.Algebra.GroupWithZero.Defs |
modifiedExponentiation with zeroc30264ede67b
| Field | From #1680 | To #1693 |
|---|
| note | `pow_zero : a ^ 0 = 1` (and `zero_pow` for `0 ^ n`) formalize exponentiation involving zero. | `pow_zero : a ^ 0 = 1` (with `zero_pow` for `0 ^ n`) formalizes exponentiation involving zero. |
modifiedZero element941093b3506f
| Field | From #1680 | To #1693 |
|---|
| mathlib.module | Mathlib.Algebra.Group.Defs | Init.Prelude |
modifiedZero function0510664c16eb
| Field | From #1680 | To #1693 |
|---|
| mathlib.module | Mathlib.Algebra.Group.Pi.Basic | Mathlib.Algebra.Notation.Pi.Defs |
modifiedZero to a positive power592cd8610f7a
| Field | From #1680 | To #1693 |
|---|
| mathlib.module | Mathlib.Algebra.GroupPower.Basic | Mathlib.Algebra.GroupWithZero.Basic |
modifiedZero is an integer multiple of any integerc6a2a1c555b0
| Field | From #1680 | To #1693 |
|---|
| mathlib.module | Mathlib.Algebra.Divisibility.Basic | Mathlib.Algebra.GroupWithZero.Divisibility |
addedZero is a rational and real numbere11c313e9045
addedAll rationals are algebraic72845cb7d4ac
addedZero as absorbing element for multiplication1cc5dec7b343