Revision #2319 → #2988 · back to history
modifiedSum of a finite geometric series (Book IX, Prop. 35)747957e93ad3
| Field | From #2319 | To #2988 |
|---|
| note | geom_sum_eq gives ∑ xⁱ = (xⁿ − 1)/(x − 1) in a field, the standard finite geometric-series formula. | geom_sum_eq gives ∑ xⁱ = (xⁿ − 1)/(x − 1) in a field, the standard finite geometric-series formula (verified module is Mathlib.Algebra.Field.GeomSum). |
| provenance | ai | ai-moderated |
modifiedConstruction of even perfect numbers (Book IX, Prop. 36)928720baa2b2
| Field | From #2319 | To #2988 |
|---|
| note | 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. | decl_exists confirms Nat.Perfect.two_pow_mul_mersenne_of_prime does not exist; Mathlib has Nat.Perfect and mersenne but no theorem that 2^(p−1)·(2^p−1) is perfect when 2^p−1 is prime. |
modifiedEuclid–Euler theoremd34bb58db9d4
| Field | From #2319 | To #2988 |
|---|
| note | The cited Nat.even_and_perfect_iff does not exist and no Mathlib decl characterizes even perfect numbers in terms of Mersenne primes. | decl_exists confirms Nat.even_and_perfect_iff does not exist; semantic search shows no Mathlib decl characterizes even perfect numbers via Mersenne primes. |
modifiedPasch's axiom47e0de4b20ce
| Field | From #2319 | To #2988 |
|---|
| note | Pasch's axiom — that a line entering a triangle through one side must exit through another — is not stated synthetically in Mathlib. | Pasch's axiom — that a line entering a triangle through one side must exit through another — is not stated synthetically in Mathlib, though Wbtw/Sbtw betweenness primitives exist. |
modifiedIrrationality of √2 (Book X)1232c5b7ff73
| Field | From #2319 | To #2988 |
|---|
| note | Mathlib's Nat.Prime.irrational_sqrt yields irrationality of √p for every prime p, in particular √2; an `irrational_sqrt_two` corollary is also available. | Mathlib's Nat.Prime.irrational_sqrt yields irrationality of √p for every prime p, in particular √2; a specialised irrational_sqrt_two corollary is also available. |
addedFinding the center of a circle (Book III, Prop. 1)f50e665be4dd
addedThales' theorem (mention in lead)9141c22c1e6c
addedUnit / the number one (Book VII, Def. 1)2e5f6dd54518
addedSimilarity of parallelepipeds (Book XI)2a872690a8b5