Theorem NormedSpace.normalize_eq_self_of_norm_eq_one

Modification history

2025-09-04 21:15
Mathlib/Analysis/NormedSpace/Normalize.lean
feat(Analysis.NormedSpace): add normalized vectors (#26308) …
Added NormedSpace.normalize_eq_self_of_norm_eq_oneView on Github →