Theorem AffineSubspace.signedInfDist_apply

Modification history

2025-09-01 07:30
Mathlib/Geometry/Euclidean/SignedDist.lean
feat(Geometry/Euclidean/SignedDist): `signedDist` between two points (#27260) …
Deleted AffineSubspace.signedInfDist_applyView on Github →
2025-04-07 09:08
Mathlib/Geometry/Euclidean/SignedDist.lean
chore(Geometry/Euclidean/SignedDist): rename `signedDist` to `signedInfDist` (#23646) …
Added AffineSubspace.signedInfDist_applyView on Github →