# 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_2}
{P : Type u_1}
[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`

.