Documentation

Archive.Wiedijk100Theorems.HeronsFormula

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 #

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) :
let a := dist p1 p2; let b := dist p3 p2; let c := dist p1 p3; let s := (a + b + c) / 2; 1 / 2 * a * b * Real.sin (EuclideanGeometry.angle p1 p2 p3) = (s * (s - a) * (s - b) * (s - c))

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.