Diff — 0
Revision #2883 → #3360 · back to history
modifiedNo natural precedes zero7e765c45aa41
| Field | From #2883 | To #3360 |
|---|
| mathlib.module | Init.Prelude | Init.Data.Nat.Basic |
modifiedSubtraction with zeroedced1cd07e0
| Field | From #2883 | To #3360 |
|---|
| anchor.snippet | Subtraction | x − 0 = x and 0 − x = − x |
| provenance | ai | ai-moderated |
modifiedMultiplication by zero rule48295336dd49
| Field | From #2883 | To #3360 |
|---|
| anchor.snippet | Multiplication | x · 0 = 0 · x = 0 |
| provenance | ai | ai-moderated |
modifiedExponentiation with zeroc30264ede67b
| Field | From #2883 | To #3360 |
|---|
| anchor.snippet | Exponentiation | x 0 = x / x = 1 |
| provenance | ai | ai-moderated |
added0/0 limit found by l'Hôpital's rule3caa1ee9a865
addedZero is not a natural number (convention-dependent)f67780cab7e1