Theorem Affine.Simplex.abs_signedDist_eq_dist_of_mem_affineSpan_range

Modification history

2025-04-07 09:08
Mathlib/Geometry/Euclidean/SignedDist.lean
chore(Geometry/Euclidean/SignedDist): rename `signedDist` to `signedInfDist` (#23646) …
Deleted Affine.Simplex.abs_signedDist_eq_dist_of_mem_affineSpan_rangeView on Github →
2025-03-31 13:41
Mathlib/Geometry/Euclidean/SignedDist.lean
feat(Geometry/Euclidean/SignedDist): signed distance between affine subspace and point (#22751) …
Added Affine.Simplex.abs_signedDist_eq_dist_of_mem_affineSpan_rangeView on Github →