Revision #1350 → #1837 · back to history
modifiedThird side from two sides and included anglee15f26deb63e
| Field | From #1350 | To #1837 |
|---|
| anchors | [{"section":"Use in solving triangles","snippet":"the third side of a triangle if two sides and the angle between them is known"},{"type":"math_alttext","value":"{\\displaystyle c={\\sqrt {a^{2}+b^{2}-2ab\\cos \\gamma }}\\,;}"}] | — |
modifiedAngles from three sides37218d7ca148
| Field | From #1350 | To #1837 |
|---|
| anchors | [{"section":"Use in solving triangles","snippet":"the angles of a triangle if the three sides are known"},{"type":"math_alttext","value":"{\\displaystyle \\gamma =\\arccos \\left({\\frac {a^{2}+b^{2}-c^{2}}{2ab}}\\right)\\,;}"}] | — |
modifiedThird side from two sides and non-included angle166692d5205c
| Field | From #1350 | To #1837 |
|---|
| anchors | [{"section":"Use in solving triangles","snippet":"the third side of a triangle if two sides and an angle opposite to one of them is known"},{"type":"math_alttext","value":"{\\displaystyle a=b\\cos \\gamma \\pm {\\sqrt {c^{2}-b^{2}\\sin ^{2}\\gamma }}\\,.}"}] | — |
modifiedAl-Kāshī's formula (acute case)80419e015ac0
| Field | From #1350 | To #1837 |
|---|
| mathlib.match_kind | exact | invocation |
| note | Same statement as the modern law of cosines `law_cos`. | Al-Kāshī's form `c = √((b - a cos γ)² + (a sin γ)²)` is mathematically equivalent to `law_cos` after squaring and applying the Pythagorean identity, but the unsquared form is not a separate Mathlib lemma. |
| provenance | ai | ai-moderated |
| status | formalized | partial |
modifiedAl-Kāshī's formula (obtuse case)40dbf0b2210f
| Field | From #1350 | To #1837 |
|---|
| mathlib.match_kind | exact | invocation |
| note | Identical to `law_cos`, which handles both acute and obtuse uniformly. | Obtuse-case unsquared form is equivalent to `law_cos` after expansion; no separate Mathlib lemma. |
| provenance | ai | ai-moderated |
| status | formalized | partial |
modifiedPythagorean theorem applied to triangle AHBc0501a040649
| Field | From #1350 | To #1837 |
|---|
| anchors | [{"section":"Case of an obtuse angle","snippet":"triangle AHB gives us"},{"type":"math_alttext","value":"{\\displaystyle c^{2}=(b+d)^{2}+h^{2},}"}] | — |
modifiedPythagorean theorem applied to triangle CHBe3032a9229dc
| Field | From #1350 | To #1837 |
|---|
| anchors | [{"section":"Case of an obtuse angle","snippet":"and triangle CHB gives"},{"type":"math_alttext","value":"{\\displaystyle d^{2}+h^{2}=a^{2}.}"}] | — |
modifiedEuclid's Proposition 12 derivation951c06d49812
| Field | From #1350 | To #1837 |
|---|
| anchors | [{"section":"Case of an obtuse angle","snippet":"This is Euclid's Proposition 12 from Book 2 of the Elements"},{"type":"math_alttext","value":"{\\displaystyle d=a\\cos(\\pi -\\gamma )=-a\\cos \\gamma .}"}] | — |
modifiedSecond angle from two sides and included anglea051289c1c1a
| Field | From #1350 | To #1837 |
|---|
| anchors | [{"section":"Another proof in the acute case","snippet":"if the angle opposite side a is α then"},{"type":"math_alttext","value":"{\\displaystyle \\tan \\alpha ={\\frac {a\\sin \\gamma }{b-a\\cos \\gamma }}.}"}] | — |
modifiedAltitude decomposition of side cdfb446d44ade
| Field | From #1350 | To #1837 |
|---|
| anchors | [{"section":"From three altitudes","snippet":"Each of these distances can be written as one of the other sides multiplied by the cosine of the adjacent angle"},{"type":"math_alttext","value":"{\\displaystyle c=a\\cos \\beta +b\\cos \\alpha .}"}] | — |
modifiedMultiplying by c yields side relation2733fdbd72e4
| Field | From #1350 | To #1837 |
|---|
| anchors | [{"section":"From three altitudes","snippet":"Multiplying both sides by c yields"},{"type":"math_alttext","value":"{\\displaystyle c^{2}=ac\\cos \\beta +bc\\cos \\alpha .}"}] | — |
modifiedAnalogous equations for other sides9990dfccaac8
| Field | From #1350 | To #1837 |
|---|
| anchors | [{"section":"From three altitudes","snippet":"The same steps work just as well when treating either of the other sides as the base of the triangle"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}a^{2}&=ac\\cos \\beta +ab\\cos \\gamma ,\\\\[3mu]b^{2}&=bc\\cos \\alpha +ab\\cos \\gamma .\\end{aligned}}}"}] | — |
modifiedLaw of cosines via subtraction of altitude equations2b6c3c2f3f5f
| Field | From #1350 | To #1837 |
|---|
| anchors | [{"section":"From three altitudes","snippet":"and subtracting the equations for"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}c^{2}-a^{2}-b^{2}&={\\color {BlueGreen}{\\cancel {\\color {Black}ac\\cos \\beta }}}+{\\color {Peach}{\\cancel {\\color {Black}bc\\cos \\alpha }}}-{\\color {BlueGreen}{\\cancel {\\color {Black}ac\\cos \\beta }}}-{\\color {Peach}{\\cancel {\\color {Black}bc\\cos \\alpha }}}-2ab\\cos \\gamma \\\\c^{2}&=a^{2}+b^{2}-2ab\\cos \\gamma .\\end{aligned}}}"}] | — |
modifiedLaw of cosines via Cartesian coordinates0592beb8c8d1
| Field | From #1350 | To #1837 |
|---|
| anchors | [{"section":"Cartesian coordinates","snippet":"Squaring both sides and simplifying"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}c^{2}&=(a-b\\cos \\theta )^{2}+(-b\\sin \\theta )^{2}\\\\&=a^{2}-2ab\\cos \\theta +b^{2}\\cos ^{2}\\theta +b^{2}\\sin ^{2}\\theta \\\\&=a^{2}+b^{2}(\\sin ^{2}\\theta +\\cos ^{2}\\theta )-2ab\\cos \\theta \\\\&=a^{2}+b^{2}-2ab\\cos \\theta .\\end{aligned}}}"}] | — |
modifiedConstruction for Ptolemy proof544573ad40f0
| Field | From #1350 | To #1837 |
|---|
| anchors | [{"section":"Using Ptolemy's theorem","snippet":"Triangle ABD is constructed congruent to triangle ABC"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}&BF=AE=BC\\cos {\\hat {B}}=a\\cos {\\hat {B}}\\\\\\Rightarrow \\ &DC=EF=AB-2BF=c-2a\\cos {\\hat {B}}.\\end{aligned}}}"}] | — |
modifiedLaw of cosines via Ptolemy's theorem2718da346701
| Field | From #1350 | To #1837 |
|---|
| anchors | [{"section":"Using Ptolemy's theorem","snippet":"the law of cosines is rendered by a straightforward application of Ptolemy's theorem to cyclic quadrilateral ABCD"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}&AD\\times BC+AB\\times DC=AC\\times BD\\\\\\Rightarrow \\ &a^{2}+c(c-2a\\cos {\\hat {B}})=b^{2}\\\\\\Rightarrow \\ &a^{2}+c^{2}-2ac\\cos {\\hat {B}}=b^{2}.\\end{aligned}}}"}] | — |
modifiedPythagorean theorem as special case via Ptolemy0f442198c425
| Field | From #1350 | To #1837 |
|---|
| anchors | [{"section":"Using Ptolemy's theorem","snippet":"Plainly if angle B is right , then ABCD is a rectangle and application of Ptolemy's theorem yields the Pythagorean theorem"},{"type":"math_alttext","value":"{\\displaystyle a^{2}+c^{2}=b^{2}.}"}] | — |
modifiedAcute case area equality19319a12ef88
| Field | From #1350 | To #1837 |
|---|
| anchors | [{"section":"By comparing areas","snippet":"The equality of areas on the left and on the right gives"},{"type":"math_alttext","value":"{\\displaystyle a^{2}+b^{2}=c^{2}+2ab\\cos \\gamma .}"}] | — |
modifiedPythagorean theorem on yellow triangle (acute, a>2b cos γ)a89ed9f9d8bb
| Field | From #1350 | To #1837 |
|---|
| anchors | [{"section":"Using circle geometry","snippet":"so the yellow triangle in Figure 8 is right. Apply the Pythagorean theorem to obtain"},{"type":"math_alttext","value":"{\\displaystyle c^{2}=b^{2}+h^{2}.}"}] | — |
modifiedTangent-secant theoremf12594d2b8c2
| Field | From #1350 | To #1837 |
|---|
| anchors | [{"section":"Using circle geometry","snippet":"the square on the tangent through a point B outside the circle is equal to the product of the two lines segments"},{"type":"math_alttext","value":"{\\displaystyle h^{2}=a(a-2b\\cos \\gamma ).}"}] | — |
modifiedLaw of cosines via tangent-secant531f8e5792c5
| Field | From #1350 | To #1837 |
|---|
| anchors | [{"section":"Using circle geometry","snippet":"Substituting into the previous equation gives the law of cosines"},{"type":"math_alttext","value":"{\\displaystyle c^{2}=b^{2}+a(a-2b\\cos \\gamma ).}"}] | — |
modifiedPythagorean theorem applied (acute, a<2b cos γ)a794a90e091d
| Field | From #1350 | To #1837 |
|---|
| anchors | [{"section":"Using circle geometry","snippet":"and a chord through B perpendicular to"},{"type":"math_alttext","value":"{\\displaystyle b^{2}=c^{2}+h^{2}.}"}] | — |
modifiedChord theoremd25a807b0ca3
| Field | From #1350 | To #1837 |
|---|
| anchors | [{"section":"Using circle geometry","snippet":"if two chords intersect, the product of the two line segments obtained on one chord is equal to the product of the two line segments obtained on the other chord"},{"type":"math_alttext","value":"{\\displaystyle h^{2}=a(2b\\cos \\gamma -a).}"}] | — |
modifiedLaw of cosines via power of point (obtuse)0634b14fe7dd
| Field | From #1350 | To #1837 |
|---|
| anchors | [{"section":"Using circle geometry","snippet":"This proof uses the power of a point theorem directly"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}c^{2}-a^{2}&{}=b(b+2a\\cos(\\pi -\\gamma ))\\\\&{}=b(b-2a\\cos \\gamma ),\\end{aligned}}}"}] | — |
modifiedLaw of sinesdbb1aade1c7e
| Field | From #1350 | To #1837 |
|---|
| anchors | [{"section":"Using the law of sines","snippet":"The law of sines holds that"},{"type":"math_alttext","value":"{\\displaystyle {\\frac {a}{\\sin \\alpha {\\vphantom {\\beta }}}}={\\frac {b}{\\sin \\beta }}={\\frac {c}{\\sin \\gamma {\\vphantom {\\beta }}}}=k,}"}] | — |
modifiedDot product proof of law of cosinesbc3c986d9c99
| Field | From #1350 | To #1837 |
|---|
| anchors | [{"section":"Using vectors","snippet":"Taking the dot product of each side with itself"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}{\\vec {c}}\\cdot {\\vec {c}}&=({\\vec {a}}-{\\vec {b}})\\cdot ({\\vec {a}}-{\\vec {b}})\\\\\\Vert {\\vec {c}}\\Vert ^{2}&=\\Vert {\\vec {a}}\\Vert ^{2}+\\Vert {\\vec {b}}\\Vert ^{2}-2\\,{\\vec {a}}\\cdot {\\vec {b}}\\end{aligned}}}"}] | — |
addedPolarization identity for ‖a−b‖²98ede2cfcd90
modifiedIsosceles simplification of law of cosinesa8d052f7fe9f
| Field | From #1350 | To #1837 |
|---|
| anchors | [{"section":"Isosceles case","snippet":"the law of cosines becomes"},{"type":"math_alttext","value":"{\\displaystyle \\cos \\gamma =1-{\\frac {c^{2}}{2a^{2}}}}"}] | — |
modifiedLaw of cosines for tetrahedraa17c4e1faa0e
| Field | From #1350 | To #1837 |
|---|
| anchors | [{"section":"Analogue for tetrahedra","snippet":"a higher-dimensional analogue of the law of cosines is"},{"type":"math_alttext","value":"{\\displaystyle A^{2}=B^{2}+C^{2}+D^{2}-2\\left(BC\\cos \\varphi _{bc}+CD\\cos \\varphi _{cd}+DB\\cos \\varphi _{db}\\right).}"}] | — |
modifiedSmall-angle (haversine-like) form of law of cosines0e8f77f5b2a1
| Field | From #1350 | To #1837 |
|---|
| anchors | [{"section":"Version suited to small angles","snippet":"a mathematically equivalent version of the law of cosines, similar to the haversine formula , can prove useful"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}c^{2}&=(a-b)^{2}+4ab\\sin ^{2}\\left({\\frac {\\gamma }{2}}\\right)\\\\&=(a-b)^{2}+4ab\\operatorname {haversin} (\\gamma ).\\end{aligned}}}"}] | — |
modifiedHyperbolic law of cosines (first)be9d68c608a9
| Field | From #1350 | To #1837 |
|---|
| anchors | [{"section":"In non-Euclidean geometry","snippet":"a pair of equations are collectively known as the hyperbolic law of cosines"},{"type":"math_alttext","value":"{\\displaystyle \\cosh a=\\cosh b\\cosh c-\\sinh b\\sinh c\\cos A}"}] | — |
modifiedHyperbolic law of cosines (second)21149d62f5fc
| Field | From #1350 | To #1837 |
|---|
| anchors | [{"section":"In non-Euclidean geometry","snippet":"and the second is"},{"type":"math_alttext","value":"{\\displaystyle \\cos A=-\\cos B\\cos C+\\sin B\\sin C\\cosh a.}"}] | — |