Theorem NormedSpace.normalize_smul

Modification history

2025-09-23 16:16
Mathlib/Analysis/NormedSpace/Normalize.lean
chore(Geometry/Euclidean/SignedDist): use `normalize` (#29897) …
Added NormedSpace.normalize_smulView on Github →