Revision #1506 → #1850 · back to history
modifiedPythagorean equation972c235fc458
| Field | From #1506 | To #1850 |
|---|
| anchors | [{"section":"(Lead)","snippet":"sometimes called the Pythagorean equation"},{"type":"math_alttext","value":"{\\displaystyle a^{2}+b^{2}=c^{2}.}"}] | — |
| mathlib.match_kind | exact | special_case |
| note | The equation a²+b²=c² is captured by the definition `PythagoreanTriple x y z : x*x + y*y = z*z`. | The equation a²+b²=c² is captured by `PythagoreanTriple x y z : x*x + y*y = z*z`; Mathlib's predicate is the integer-restricted special case of the real-side equation. |
| provenance | ai | ai-moderated |
modifiedAlgebraic proof with four triangles around square of side cb05f5126884d
| Field | From #1506 | To #1850 |
|---|
| anchors | [{"section":"Algebraic proofs","snippet":"proved algebraically using four copies of the same triangle arranged symmetrically around a square with side c"},{"type":"math_alttext","value":"{\\displaystyle (b+a)^{2}=c^{2}+4{\\frac {ab}{2}}=c^{2}+2ab,}"},{"type":"math_alttext","value":"{\\displaystyle c^{2}=(b+a)^{2}-2ab=b^{2}+2ab+a^{2}-2ab=a^{2}+b^{2}.}"}] | — |
modifiedAlgebraic proof with triangles inside square of side c4a9f5baf22dc
| Field | From #1506 | To #1850 |
|---|
| anchors | [{"section":"Algebraic proofs","snippet":"A similar proof uses four copies of a right triangle"},{"type":"math_alttext","value":"{\\displaystyle (b-a)^{2}+4{\\frac {ab}{2}}=(b-a)^{2}+2ab=b^{2}-2ab+a^{2}+2ab=a^{2}+b^{2}.}"}] | — |
addedTriangle postulate (angle sum)17f9d9b90646
modifiedGarfield's trapezoid proof290e04607fd6
| Field | From #1506 | To #1850 |
|---|
| anchors | [{"section":"Other algebraic proofs","snippet":"A related proof by U.S. president James A. Garfield"},{"type":"math_alttext","value":"{\\displaystyle {\\tfrac {1}{2}}(b+a)^{2}.}"}] | — |
modifiedDijkstra's formulation217d3a30080c
| Field | From #1506 | To #1850 |
|---|
| anchors | [{"section":"Converse","snippet":"Edsger W. Dijkstra has stated this proposition about acute, right, and obtuse triangles"},{"type":"math_alttext","value":"{\\displaystyle \\operatorname {sgn} (\\alpha +\\beta -\\gamma )=\\operatorname {sgn} (a^{2}+b^{2}-c^{2}),}"}] | — |
modifiedEuclid's formula for Pythagorean triplesd81026aee88e
| Field | From #1506 | To #1850 |
|---|
| anchors | [{"section":"Pythagorean triples","snippet":"Euclid's formula is the most well-known"},{"type":"math_alttext","value":"{\\displaystyle a=m^{2}-n^{2},\\quad b=2mn,\\quad c=m^{2}+n^{2}}"}] | — |
modifiedInverse (reciprocal) Pythagorean theorem8cef2d064d0b
| Field | From #1506 | To #1850 |
|---|
| anchors | [{"section":"Inverse Pythagorean theorem","snippet":"the inverse Pythagorean theorem relates the two legs"},{"type":"math_alttext","value":"{\\displaystyle a^{2}+b^{2}=c^{2}}"},{"type":"math_alttext","value":"{\\displaystyle {\\frac {1}{a^{2}}}+{\\frac {1}{b^{2}}}={\\frac {1}{d^{2}}}}"},{"type":"math_alttext","value":"{\\displaystyle {\\frac {1}{(xz)^{2}}}+{\\frac {1}{(yz)^{2}}}={\\frac {1}{(xy)^{2}}}}"},{"type":"math_alttext","value":"{\\displaystyle {\\frac {1}{20^{2}}}+{\\frac {1}{15^{2}}}={\\frac {1}{12^{2}}}}"},{"type":"math_alttext","value":"{\\displaystyle {\\frac {1}{p}}+{\\frac {1}{q}}={\\frac {1}{r}}}"}] | — |
modifiedModulus of a complex numberd9456a8278a4
| Field | From #1506 | To #1850 |
|---|
| anchors | [{"section":"Complex numbers","snippet":"the absolute value or modulus is given by"},{"type":"math_alttext","value":"{\\displaystyle z=x+iy,}"},{"type":"math_alttext","value":"{\\displaystyle r=|z|={\\textstyle {\\sqrt {x^{2}+y^{2}}}}.}"},{"type":"math_alttext","value":"{\\displaystyle r^{2}=x^{2}+y^{2}.}"}] | — |
| mathlib.module | Mathlib.Analysis.SpecialFunctions.PolarCoord | Mathlib.Data.Complex.Basic |
| note | Complex.normSq z = z.re^2 + z.im^2, and `Complex.norm_def` / `‖z‖` give the modulus √(re²+im²). | `Complex.normSq z = z.re^2 + z.im^2`, and the norm `‖z‖` is the square root, giving the modulus formula. |
modifiedDistance between complex numbers9ab6489c1c71
| Field | From #1506 | To #1850 |
|---|
| anchors | [{"section":"Complex numbers","snippet":"This can be generalised to find the distance between two points"},{"type":"math_alttext","value":"{\\displaystyle |z_{1}-z_{2}|={\\sqrt {(x_{1}-x_{2})^{2}+(y_{1}-y_{2})^{2}}},}"},{"type":"math_alttext","value":"{\\displaystyle |z_{1}-z_{2}|^{2}=(x_{1}-x_{2})^{2}+(y_{1}-y_{2})^{2}.}"}] | — |
| mathlib.module | Mathlib.Analysis.SpecialFunctions.Complex.CircleMap | Mathlib.Analysis.Complex.Norm |
modifiedEuclidean distance in the plane78d77957a06e
| Field | From #1506 | To #1850 |
|---|
| note | The 2D case is the n=2 instance of the n-dimensional EuclideanSpace.dist_eq formula. | The 2D case is the n=2 instance of the n-dimensional `EuclideanSpace.dist_eq` formula. |
modifiedPythagorean trigonometric identity33e1c497e4d7
| Field | From #1506 | To #1850 |
|---|
| anchors | [{"section":"Pythagorean trigonometric identity","snippet":"the fundamental Pythagorean trigonometric identity"},{"type":"math_alttext","value":"{\\displaystyle {\\cos }^{2}\\theta +{\\sin }^{2}\\theta ={\\frac {a^{2}+b^{2}}{c^{2}}}=1,}"}] | — |
| mathlib.module | Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic | Mathlib.Analysis.Complex.Trigonometric |
modifiedPythagorean relation between cross product and dot product33034e81ae5a
| Field | From #1506 | To #1850 |
|---|
| anchors | [{"section":"Relation to the cross product","snippet":"The Pythagorean theorem relates the cross product and dot product"},{"type":"math_alttext","value":"{\\displaystyle \\|\\mathbf {a} \\times \\mathbf {b} \\|^{2}+(\\mathbf {a} \\cdot \\mathbf {b} )^{2}=\\|\\mathbf {a} \\|^{2}\\|\\mathbf {b} \\|^{2}.}"}] | — |
modifiedLaw of cosines48e51b784377
| Field | From #1506 | To #1850 |
|---|
| anchors | [{"section":"Law of cosines","snippet":"a special case of the more general theorem relating the lengths of sides in any triangle"},{"type":"math_alttext","value":"{\\displaystyle a^{2}+b^{2}-2ab\\cos {\\theta }=c^{2}}"}] | — |
modifiedThābit ibn Qurra's generalization1bd229146962
| Field | From #1506 | To #1850 |
|---|
| anchors | [{"section":"Arbitrary triangle","snippet":"Thābit ibn Qurra stated that the sides of the three triangles were related as"},{"type":"math_alttext","value":"{\\displaystyle a^{2}+b^{2}=c(r+s).}"}] | — |
modifiedCuboid diagonal via Pythagorase2c707229356
| Field | From #1506 | To #1850 |
|---|
| anchors | [{"section":"Solid geometry","snippet":"The length of face diagonal AC is found from Pythagoras's theorem"},{"type":"math_alttext","value":"{\\displaystyle {\\overline {AC}}^{\\,2}={\\overline {AB}}^{\\,2}+{\\overline {BC}}^{\\,2},}"}] | — |
| note | Follows directly from EuclideanSpace.dist_sq_eq in ℝ³, but no specific cuboid-diagonal lemma is named. | Follows directly from `EuclideanSpace.dist_sq_eq` in ℝ³, but no specific cuboid-diagonal lemma is named. |
modifiedPythagorean theorem in inner product spaces67f4d862629b
| Field | From #1506 | To #1850 |
|---|
| anchors | [{"section":"Inner product spaces","snippet":"In an inner-product space, the Pythagorean theorem states that for any two orthogonal vectors"},{"type":"math_alttext","value":"{\\displaystyle \\left\\|\\mathbf {v} +\\mathbf {w} \\right\\|^{2}=\\left\\|\\mathbf {v} \\right\\|^{2}+\\left\\|\\mathbf {w} \\right\\|^{2}.}"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}\\left\\|\\mathbf {v} +\\mathbf {w} \\right\\|^{2}&=\\langle \\mathbf {v+w} ,\\ \\mathbf {v+w} \\rangle \\\\[3mu]&=\\langle \\mathbf {v} ,\\,\\mathbf {v} \\rangle +\\langle \\mathbf {w} ,\\,\\mathbf {w} \\rangle +\\langle \\mathbf {v,\\,w} \\rangle +\\langle \\mathbf {w,\\,v} \\rangle \\\\[3mu]&=\\left\\|\\mathbf {v} \\right\\|^{2}+\\left\\|\\mathbf {w} \\right\\|^{2},\\end{aligned}}}"}] | — |
modifiedParallelogram lawd6646db9856d
| Field | From #1506 | To #1850 |
|---|
| anchors | [{"section":"Inner product spaces","snippet":"the parallelogram law"},{"type":"math_alttext","value":"{\\displaystyle 2\\|\\mathbf {v} \\|^{2}+2\\|\\mathbf {w} \\|^{2}=\\|\\mathbf {v+w} \\|^{2}+\\|\\mathbf {v-w} \\|^{2},}"}] | — |
modifiedPythagorean identity for n orthogonal vectors14b3a01f8eaa
| Field | From #1506 | To #1850 |
|---|
| anchors | [{"section":"Inner product spaces","snippet":"The Pythagorean identity can be extended to sums of more than two orthogonal vectors"},{"type":"math_alttext","value":"{\\displaystyle {\\biggl \\|}\\sum _{k=1}^{n}\\mathbf {v} _{k}{\\biggr \\|}^{2}=\\sum _{k=1}^{n}\\|\\mathbf {v} _{k}\\|^{2}}"}] | — |
modifiedSpherical Pythagorean theoremd175b8f63a15
| Field | From #1506 | To #1850 |
|---|
| anchors | [{"section":"Spherical geometry","snippet":"For any right triangle on a sphere of radius R"},{"type":"math_alttext","value":"{\\displaystyle \\cos {\\frac {c}{R}}=\\cos {\\frac {a}{R}}\\,\\cos {\\frac {b}{R}}.}"}] | — |
modifiedSpherical law of cosines419ecc509391
| Field | From #1506 | To #1850 |
|---|
| anchors | [{"section":"Spherical geometry","snippet":"the spherical law of cosines that applies to all spherical triangles"},{"type":"math_alttext","value":"{\\displaystyle \\cos {\\frac {c}{R}}=\\cos {\\frac {a}{R}}\\,\\cos {\\frac {b}{R}}+\\sin {\\frac {a}{R}}\\,\\sin {\\frac {b}{R}}\\,\\cos {\\gamma }.}"}] | — |
modifiedHyperbolic Pythagorean theorem542754e845ff
| Field | From #1506 | To #1850 |
|---|
| anchors | [{"section":"Hyperbolic geometry","snippet":"In a hyperbolic space with uniform Gaussian curvature"},{"type":"math_alttext","value":"{\\displaystyle \\cosh {\\frac {c}{R}}=\\cosh {\\frac {a}{R}}\\,\\cosh {\\frac {b}{R}}}"}] | — |
modifiedHyperbolic law of cosines0e3d1d72a396
| Field | From #1506 | To #1850 |
|---|
| anchors | [{"section":"Hyperbolic geometry","snippet":"the hyperbolic law of cosines that applies to all hyperbolic triangles"},{"type":"math_alttext","value":"{\\displaystyle \\cosh {\\frac {c}{R}}=\\cosh {\\frac {a}{R}}\\,\\cosh {\\frac {b}{R}}-\\sinh {\\frac {a}{R}}\\,\\sinh {\\frac {b}{R}}\\,\\cos \\gamma ,}"}] | — |
modifiedPythagorean theorem for very small triangles under uniform curvature9b25b8703e16
| Field | From #1506 | To #1850 |
|---|
| anchors | [{"section":"Very small triangles","snippet":"For any uniform curvature K (positive, zero, or negative), in very small right triangles"},{"type":"math_alttext","value":"{\\displaystyle c^{2}=a^{2}+b^{2}-{\\frac {K}{3}}a^{2}b^{2}-{\\frac {K^{2}}{45}}a^{2}b^{2}(a^{2}+b^{2})-{\\frac {2K^{3}}{945}}a^{2}b^{2}(a^{2}-b^{2})^{2}+O(K^{4}c^{10}).}"}] | — |
modifiedRiemannian metric tensorfc85ea5ecbeb
| Field | From #1506 | To #1850 |
|---|
| anchors | [{"section":"Differential geometry","snippet":"which is called the metric tensor"},{"type":"math_alttext","value":"{\\displaystyle ds^{2}=dr^{2}+r^{2}d\\theta ^{2}.}"}] | — |
| mathlib.decl | RiemannianBundle | Bundle.RiemannianMetric |
| note | A Riemannian metric is formalized as an inner product on each fiber of a vector bundle via `RiemannianBundle` / `IsRiemannianManifold`. | A Riemannian metric is formalized as a family of inner products on the fibers of a vector bundle via `Bundle.RiemannianMetric` (with `Bundle.RiemannianBundle` for typeclass inference). |