Theorem Affine.Simplex.ExcenterExists.affineSpan_faceOpposite_eq_orthRadius

Modification history

2025-12-10 20:52
Mathlib/Geometry/Euclidean/Incenter.lean
feat(Geometry/Euclidean/Incenter): `orthRadius` lemmas (#31733) …
Added Affine.Simplex.ExcenterExists.affineSpan_faceOpposite_eq_orthRadiusView on Github →