normalize_zero_eq_zero

Mathlib.Analysis.NormedSpace.Normalize

URI: https://scilib.ai/kg/mathlib#NormedSpace.normalize_zero_eq_zero

English

The normalization of zero is zero: normalize(0) = 0.

Русский

Нормализация нуля равна нулю: normalize(0) = 0.

LaTeX

$$$\\text{normalize}(0)=0$$$

Lean4

@[simp]
theorem normalize_zero_eq_zero : normalize (0 : V) = 0 := by simp [normalize]

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru