Commit 2025-09-04 21:15 737db8d1

View on Github →

feat(Analysis.NormedSpace): add normalized vectors (#26308) Add normalized vectors to Mathlib (zero vector for zero vector, the corresponding unit vectors for nonzero vectors)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/NormedSpace/Normalize.lean

added theorem NormedSpace.norm_normalize_eq_one_iff

added theorem NormedSpace.norm_smul_normalize

added theorem NormedSpace.normalize_eq_self_of_norm_eq_one

added theorem NormedSpace.normalize_neg

added theorem NormedSpace.normalize_normalize

added theorem NormedSpace.normalize_smul_of_neg

added theorem NormedSpace.normalize_smul_of_pos

added theorem NormedSpace.normalize_zero_eq_zero