Brahmaguptas_Formula
Provedgeometryproofwiki
The area of a cyclic quadrilateral with sides a, b, c, d is sqrt((s-a)(s-b)(s-c)(s-d)) where s = (a+b+c+d)/2.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Brahmaguptas_Formula (a b c d : ℝ) (ha : a > 0) (hb : b > 0) (hc : c > 0) (hd : d > 0) (s : ℝ) (hs : s = (a + b + c + d) / 2) (area : ℝ) (h : area = Real.sqrt ((s - a) * (s - b) * (s - c) * (s - d))) : area = Real.sqrt ((s - a) * (s - b) * (s - c) * (s - d)) := by sorry
Source