Theorem Affine.Simplex.affineSpan_faceOpposite_eq_orthRadius_insphere

Modification history

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