Theorem NormedSpace.normalize_neg

Modification history

2025-12-17 21:56
Mathlib/Analysis/Normed/Module/Normalize.lean
chore(Analysis): fix whitespace (#32909) …
Modified NormedSpace.normalize_negView on Github →
2025-09-04 21:15
Mathlib/Analysis/NormedSpace/Normalize.lean
feat(Analysis.NormedSpace): add normalized vectors (#26308) …
Added NormedSpace.normalize_negView on Github →