Theorem AffineSubspace.abs_signedInfDist_eq_dist_of_mem_affineSpan_insert

Modification history

2025-04-07 09:08
Mathlib/Geometry/Euclidean/SignedDist.lean
chore(Geometry/Euclidean/SignedDist): rename `signedDist` to `signedInfDist` (#23646) …
Added AffineSubspace.abs_signedInfDist_eq_dist_of_mem_affineSpan_insertView on Github →