Theorem signedDist_eq_dist_iff_vsub_mem_span

Modification history

2025-09-01 07:30

Mathlib/Geometry/Euclidean/SignedDist.lean

feat(Geometry/Euclidean/SignedDist): `signedDist` between two points (#27260) …

Added signedDist_eq_dist_iff_vsub_mem_span View on Github →