mathlib3 documentation

mathlib-archive / wiedijk_100_theorems.herons_formula

Freek № 57: Heron's Formula #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

source
theorem theorems_100.heron {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {p1 p2 p3 : P} (h1 : p1 ≠ p2) (h2 : p3 ≠ p2) :
let a : ℝ := has_dist.dist p1 p2, b : ℝ := has_dist.dist p3 p2, c : ℝ := has_dist.dist p1 p3, s : ℝ := (a + b + c) / 2 in 1 / 2 * a * b * real.sin (euclidean_geometry.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.