Revision #1819 → #2319 · back to history
modifiedPons asinorum (Book I, Prop. 5)76ecea39726d
| Field | From #1819 | To #2319 |
|---|
| mathlib.decl | — | EuclideanGeometry.angle_eq_angle_of_dist_eq |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Geometry.Euclidean.Triangle |
| note | No declaration in Mathlib stating that the base angles of an isosceles triangle are equal. | Mathlib's EuclideanGeometry.angle_eq_angle_of_dist_eq states that if dist p₁ p₂ = dist p₁ p₃ then angle p₁ p₂ p₃ = angle p₁ p₃ p₂, the pons asinorum. |
| status | not_formalized | formalized |
modifiedConstruction of even perfect numbers (Book IX, Prop. 36)928720baa2b2
| Field | From #1819 | To #2319 |
|---|
| note | The Euclid construction 2^(p−1)(2^p − 1) → perfect when 2^p − 1 is prime is not present in Mathlib. | The cited Nat.Perfect.two_pow_mul_mersenne_of_prime does not exist; loogle/grep show no Mathlib formalization that 2^(p−1)·(2^p−1) is perfect when 2^p−1 is prime. |
| provenance | ai | ai-moderated |
modifiedEuclid–Euler theoremd34bb58db9d4
| Field | From #1819 | To #2319 |
|---|
| mathlib.decl | mersenne | — |
| mathlib.module | Mathlib.NumberTheory.LucasLehmer | — |
| note | Mathlib has Nat.Perfect and the mersenne function/LucasLehmer test, but no theorem characterizing even perfect numbers as 2^(p−1)·(2^p − 1) with 2^p−1 prime. | The cited Nat.even_and_perfect_iff does not exist and no Mathlib decl characterizes even perfect numbers in terms of Mersenne primes. |
| provenance | ai | ai-moderated |
| status | partial | not_formalized |
addedIrrationality of √2 (Book X)1232c5b7ff73
addedAlternation of proportions (Book V, Prop. 16)b269818617bd
addedConstruction of the five Platonic solids inscribed in a sphere (Book XIII)69774eca7050
addedEuler's polyhedron formula V − E + F = 2d7a9d32b66c9
addedGeometric progression as continued proportion (Book VIII)5e95dff195d5