Theorem NormedSpace.norm_normalize_eq_one_iff

Modification history

2025-09-23 16:16
Mathlib/Analysis/NormedSpace/Normalize.lean
chore(Geometry/Euclidean/SignedDist): use `normalize` (#29897) …
Modified NormedSpace.norm_normalize_eq_one_iffView on Github →
2025-09-04 21:15
Mathlib/Analysis/NormedSpace/Normalize.lean
feat(Analysis.NormedSpace): add normalized vectors (#26308) …
Added NormedSpace.norm_normalize_eq_one_iffView on Github →