Freek № 57: Heron's Formula #
This file proves Theorem 57 from the 100 Theorems List, also known as Heron's formula, which gives the area of a triangle based only on its three sides' lengths.
References #
- https://en.wikipedia.org/wiki/Herons_formula
theorem
Theorems100.heron
{V : Type u_1}
{P : Type u_2}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[MetricSpace P]
[NormedAddTorsor V P]
{p1 : P}
{p2 : P}
{p3 : P}
(h1 : p1 ≠ p2)
(h2 : p3 ≠ p2)
:
Heron's formula: The area of a triangle with side lengths a, b, and c is
√(s * (s - a) * (s - b) * (s - c)) where s = (a + b + c) / 2 is the semiperimeter.
We show this by equating this formula to a * b * sin γ, where γ is the angle opposite
the side c.