Revision #2304 → #2589 · back to history
modifiedPythagorean theorem312faa0615c2
| Field | From #2304 | To #2589 |
|---|
| mathlib.decl | norm_add_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two | InnerProductGeometry.norm_add_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two |
| provenance | ai | ai-moderated |
modifiedEarliest statement of the Pythagorean theorem09659af06164
| Field | From #2304 | To #2589 |
|---|
| mathlib.decl | norm_add_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two | InnerProductGeometry.norm_add_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two |
| provenance | ai | ai-moderated |
modifiedThales' theorem5a2763f3bf53
| Field | From #2304 | To #2589 |
|---|
| mathlib.decl | EuclideanGeometry.thales_theorem | EuclideanGeometry.Sphere.thales_theorem |
| provenance | ai | ai-moderated |
modifiedFirst proof of the Pythagorean theoremb4500901b766
| Field | From #2304 | To #2589 |
|---|
| mathlib.decl | norm_add_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two | InnerProductGeometry.norm_add_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two |
| provenance | ai | ai-moderated |
modifiedProof of the Pythagorean theorem (Nine Chapters)4885dc598c81
| Field | From #2304 | To #2589 |
|---|
| mathlib.decl | norm_add_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two | InnerProductGeometry.norm_add_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two |
| provenance | ai | ai-moderated |
modifiedStatement of the Pythagorean theorem (Sulba Sutras)4016dcd15657
| Field | From #2304 | To #2589 |
|---|
| mathlib.decl | norm_add_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two | InnerProductGeometry.norm_add_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two |
| provenance | ai | ai-moderated |
modifiedRiemannian geometry40e91b885db1
| Field | From #2304 | To #2589 |
|---|
| mathlib.decl | riemannianEDist | Manifold.riemannianEDist |
| provenance | ai | ai-moderated |
modifiedLucas–Lehmer primality test20c830683979
| Field | From #2304 | To #2589 |
|---|
| mathlib.decl | LucasLehmer.lucas_lehmer_sufficiency | lucas_lehmer_sufficiency |
| provenance | ai | ai-moderated |
modifiedDecidability of Presburger arithmetic030a05c5a7ee
| Field | From #2304 | To #2589 |
|---|
| mathlib.decl | presburger.definable_iff_isSemilinearSet | FirstOrder.Language.presburger.definable_iff_isSemilinearSet |
| provenance | ai | ai-moderated |