Diff — 100
Revision #967 → #1973 · back to history
modified100 as natural numberf320d88099a6
| Field | From #967 | To #1973 |
|---|
| mathlib.module | Mathlib.Data.Nat.Defs | Init.Prelude |
| note | The natural number 100 is trivially expressible as the term `(100 : ℕ)` in Mathlib's `Nat` type. | The natural number 100 is the term `(100 : ℕ)` in the core `Nat` inductive type. |
modified100 is the square of 10a20b2720176b
| Field | From #967 | To #1973 |
|---|
| note | The equality `100 = 10^2` holds by `decide`/`rfl` in Mathlib, though no named lemma states this concrete fact. | The equality `100 = 10^2` is decidable in Mathlib via `decide`/`rfl`, but no named lemma states this concrete fact. |
modifiedBasis of percentagesa92f4bada979
| Field | From #967 | To #1973 |
|---|
| note | Mathlib has no definition of percentages tying to the number 100. | Mathlib has no definition of percentages tied to the number 100. |
modifiedSum of first nine primes8e18abeacc8a
| Field | From #967 | To #1973 |
|---|
| mathlib.module | Mathlib.Data.Nat.Prime.Nth | Mathlib.Data.Nat.Nth |
modifiedTotient values of 1004b729ecf279c
| Field | From #967 | To #1973 |
|---|
| note | Mathlib defines `Nat.totient` and `ArithmeticFunction.carmichael` (reduced totient) but the values at 100 are not explicit lemmas. | Mathlib defines `Nat.totient` and `ArithmeticFunction.carmichael` (reduced totient) but the values at 100 are not stated as explicit lemmas. |
modifiedNicomachus's theorem instance8a010aeef955
| Field | From #967 | To #1973 |
|---|
| note | No `sum_cubes`/Nicomachus theorem lemma was found in Mathlib via grep. | No `sum_cubes`/Nicomachus theorem lemma was found in Mathlib via grep or loogle. |
addedSquare of sum of first four positive integers3d41bdbfbb55
addedLeyland decomposition of 10006d690b871a6
modified100 is the seventeenth Erdős–Woods numberffdff60a3ba2
| Field | From #967 | To #1973 |
|---|
| anchor.snippet | is also the seventeenth Erdős–Woods number, and the fourth | is also the seventeenth Erdős–Woods number |
| label | Erdős–Woods and 18-gonal number | 100 is the seventeenth Erdős–Woods number |
| note | Neither Erdős–Woods numbers nor polygonal/18-gonal numbers appear in Mathlib by grep. | Erdős–Woods numbers are not defined in Mathlib (no matches via grep). |
| provenance | ai | ai-moderated |
added100 is the fourth 18-gonal number563bc9050fff
modified10th star number8ca9923b487f
| Field | From #967 | To #1973 |
|---|
| note | Grep for star number / starNumber in Mathlib returns no results. | Grep for `starNumber`/`star_number` in Mathlib returns no results. |