Commit 2026-11-10 23:38 350278ec

refactor(Geometry/Euclidean): promote Heron's formula to main mathlib (#44148) Now we have a proper definition of triangle's area, we can make Heron's formula an official theorem in the main library. The original proof was mostly unchanged, with only the following modification 1. Index change The naming and indexing was changed from

    let a := dist p₁ p₂
    let b := dist p₃ p₂
    let c := dist p₁ p₃

to

    let a := dist p₁ p₂
    let b := dist p₁ p₃
    let c := dist p₂ p₃

This is to follow the existing indexing convention of "1-2, 1-3, 2-3" for triangles. We have similar order for h₁₂ h₁₃ h₂₃ 2. Generalized to all degenerate cases: Removed (h1 : p₁ ≠ p₂) (h2 : p₃ ≠ p₂)