Revision #1422 → #2825 · back to history
addedOne-to-one correspondence (bijection)2152f6afb065
addedWell-ordered setfa24131deb00
modifiedPositive integers and non-negative integers4008894646cc
| Field | From #1422 | To #2825 |
|---|
| mathlib.module | Mathlib.Data.PNat.Defs | Mathlib.Data.PNat.Notation |
modifiedPeano axioms66ff56e95c78
| Field | From #1422 | To #2825 |
|---|
| mathlib.decl | Nat.rec | Nat.recAux |
| mathlib.module | — | Init.Data.Nat.Basic |
| note | `Nat` satisfies the Peano axioms (zero, injective successor, recursor `Nat.rec`), but Mathlib has no single bundled `PeanoAxioms` structure. | `Nat` satisfies the Peano axioms (zero, injective successor, recursor `Nat.recAux`), but Mathlib has no single bundled `PeanoAxioms` structure. |
addedInjectivity of successorc1061d6fe412
addedZero is not a successor0cf859019978
modifiedAxiom of induction247dd6470b21
| Field | From #1422 | To #2825 |
|---|
| mathlib.decl | Nat.rec | Nat.recAux |
| mathlib.module | — | Init.Data.Nat.Basic |
| note | The induction/recursion principle `Nat.rec` is the core recursor, with variants like `Nat.le_induction` and `Nat.strong_induction_on` in Mathlib. | The induction/recursion principle `Nat.recAux` is the core recursor, with variants like `Nat.le_induction` and `Nat.strong_induction_on` in Mathlib. |
addedAxiom of infinityaeff3a8ddbf8
addedCharacterization of ≤ via existence of c with a + c = b29053a57c462