Theorem signedDist_smul_of_neg

Modification history

2025-09-23 16:16

Mathlib/Geometry/Euclidean/SignedDist.lean

chore(Geometry/Euclidean/SignedDist): use `normalize` (#29897) …

Added signedDist_smul_of_neg View on Github →