Mathlib Changelog
v4
Changelog
About
Github
Theorem
signedDist_smul_of_pos
Modification history
2025-09-23 16:16
Mathlib/Geometry/Euclidean/SignedDist.lean
chore(Geometry/Euclidean/SignedDist): use `normalize` (#29897) …
Added
signedDist_smul_of_pos
View on Github →