Revision #2988 → #3488 · back to history
modifiedPons asinorum (Book I, Prop. 5)76ecea39726d
| Field | From #2988 | To #3488 |
|---|
| note | 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. | Verified: EuclideanGeometry.angle_eq_angle_of_dist_eq states dist p₁ p₂ = dist p₁ p₃ → angle p₁ p₂ p₃ = angle p₁ p₃ p₂, the pons asinorum. |
modifiedPythagorean theorem (Book I, Props. 47–48)764d4483eb8f
| Field | From #2988 | To #3488 |
|---|
| note | Mathlib formalizes the Pythagorean theorem in inner-product/Euclidean form as an iff with the right-angle condition. | Verified: Mathlib formalizes the Pythagorean theorem in inner-product/Euclidean form as an iff with the right-angle condition. |
modifiedGolden ratio / extreme and mean ratio (Book II, Prop. 11)c9c467bfca19
| Field | From #2988 | To #3488 |
|---|
| note | Mathlib defines Real.goldenRatio := (1 + √5)/2 together with its irrationality and algebraic identities. | Verified: Real.goldenRatio := (1 + √5)/2 with its irrationality and algebraic identities. |
modifiedInscribed angle theorem (Book III, Prop. 20)98264284fa51
| Field | From #2988 | To #3488 |
|---|
| note | Mathlib states the central-angle = 2·inscribed-angle relation for oriented angles on a circle. | Verified: Mathlib states the central-angle = 2·inscribed-angle relation for oriented angles on a circle. |
modifiedThales's theorem (Book III, Prop. 31)8b83f731271b
| Field | From #2988 | To #3488 |
|---|
| note | Mathlib's Thales' theorem states angle p₁ p₂ p₃ = π/2 iff p₂ lies on the sphere with diameter p₁p₃. | Verified: angle p₁ p₂ p₃ = π/2 iff p₂ lies on the sphere with diameter p₁p₃. |
modifiedIntersecting chords theorem (Book III, Prop. 35)2bef93b09634
| Field | From #2988 | To #3488 |
|---|
| note | Mathlib formalizes the intersecting chords theorem via cospherical points and the power-of-a-point file. | Verified: intersecting chords theorem stated via cospherical points and the power-of-a-point file. |
modifiedTangent–secant theorem (Book III, Prop. 36)2b836fe27320
| Field | From #2988 | To #3488 |
|---|
| note | Mathlib's Sphere.Power file proves the tangent–secant theorem. | Verified: Sphere.Power file proves the tangent–secant theorem. |
modifiedEuclid's theorem on infinitude of primes (Book IX, Prop. 20)b07c197005df
| Field | From #2988 | To #3488 |
|---|
| note | Nat.exists_infinite_primes proves that for every n there is a prime p ≥ n, the standard form of Euclid's theorem. | Verified: Nat.exists_infinite_primes gives ∀ n, ∃ p ≥ n, p prime — Euclid's theorem. |
modifiedSum of a finite geometric series (Book IX, Prop. 35)747957e93ad3
| Field | From #2988 | To #3488 |
|---|
| note | 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). | Verified: geom_sum_eq gives ∑ xⁱ = (xⁿ − 1)/(x − 1) in a field, the standard finite geometric-series formula. |
modifiedConstruction of even perfect numbers (Book IX, Prop. 36)928720baa2b2
| Field | From #2988 | To #3488 |
|---|
| note | 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. | Semantic search confirms Mathlib has Nat.Perfect and mersenne but no theorem that 2^(p−1)·(2^p−1) is perfect when 2^p−1 is prime. |
modifiedPerfect number755fc640e82f
| Field | From #2988 | To #3488 |
|---|
| note | Nat.Perfect n is defined exactly as the proper-divisor sum equalling n with n positive. | Verified: Nat.Perfect n is defined as the proper-divisor sum equalling n with n positive. |
modifiedEuclid–Euler theoremd34bb58db9d4
| Field | From #2988 | To #3488 |
|---|
| note | decl_exists confirms Nat.even_and_perfect_iff does not exist; semantic search shows no Mathlib decl characterizes even perfect numbers via Mersenne primes. | Semantic search shows no Mathlib decl characterizes even perfect numbers via Mersenne primes. |
modifiedIrrationality of square roots of non-square integers (Book X, Prop. 9)03e5064b8c57
| Field | From #2988 | To #3488 |
|---|
| note | Irrational (√z) ↔ ¬IsSquare z for nonneg integers, which is precisely Book X Prop 9. | Verified: Irrational (√z) ↔ ¬IsSquare z for nonneg integers — Book X Prop 9. |
modifiedEuclid's formula for Pythagorean triples (Book X, lemma to Prop. 29)c10f1d4e7b78
| Field | From #2988 | To #3488 |
|---|
| note | Mathlib classifies primitive Pythagorean triples in the (m²−n², 2mn, m²+n²) form attributed to Euclid. | Verified: Mathlib classifies primitive Pythagorean triples in the (m²−n², 2mn, m²+n²) Euclidean form. |
modifiedVolume of cone is one-third volume of cylinder (Book XII)f410ea851e19
| Field | From #2988 | To #3488 |
|---|
| note | No declaration of cone volume = (1/3)·cylinder volume appears in Mathlib. | Semantic search returns only ball-volume and category-theory 'cone' hits; no cone-vs-cylinder volume theorem exists. |
modifiedVolume of sphere proportional to cube of radius (Book XII)3500a2760720
| Field | From #2988 | To #3488 |
|---|
| note | Mathlib computes the Lebesgue volume of the 3-dimensional Euclidean ball, exhibiting the r³ proportionality. | Verified: Mathlib computes vol(ball) = r³ · (4π/3) in ℝ³, exhibiting the r³ proportionality. |
modifiedEuclidean algorithm for GCD (Book VII, Props. 1–4)aebc0ce23db9
| Field | From #2988 | To #3488 |
|---|
| note | Mathlib defines Nat.gcd by the Euclidean recursion gcd a b = gcd (b % a) a and proves the standard correctness lemmas (Nat.gcd_dvd_left, Nat.dvd_gcd, etc.). | Verified: Nat.gcd is defined by the Euclidean recursion gcd a b = gcd (b % a) a and its correctness lemmas (Nat.gcd_dvd_left, Nat.dvd_gcd) live in Mathlib's GCD/Basic. |
modifiedLaw of cosines (geometric precursor in Book II)363a54672206
| Field | From #2988 | To #3488 |
|---|
| note | Mathlib formalizes the law of cosines in inner-product space form, generalizing Euclid's geometric precursor in Book II (Propositions 12–13). | Verified: Mathlib formalizes the law of cosines in inner-product form, generalizing Book II Props 12–13. |
modifiedPasch's axiom47e0de4b20ce
| Field | From #2988 | To #3488 |
|---|
| note | 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. | 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 and sbtw_of_sbtw_of_sbtw_of_mem_affineSpan_pair exist. |
modifiedIrrationality of √2 (Book X)1232c5b7ff73
| Field | From #2988 | To #3488 |
|---|
| note | 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. | Verified: Nat.Prime.irrational_sqrt yields irrationality of √p for every prime p, in particular √2. |
modifiedThales' theorem (mention in lead)9141c22c1e6c
| Field | From #2988 | To #3488 |
|---|
| note | Same Mathlib decl as for Book III Prop. 31; Thales' theorem is that an angle inscribed in a semicircle is a right angle. | Verified: same decl as Book III Prop. 31; Thales' theorem is that an angle inscribed in a semicircle is a right angle. |
addedHyperbolic (Lobachevskian) geometry7873e1ca02ef
addedQuadrature of rectangles (Book II)0a1034db7886