norm_smul_normalize

Mathlib.Analysis.NormedSpace.Normalize

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

English

The norm of a vector times its normalization equals the vector: ||x|| · normalize(x) = x.

Русский

Норма вектора, умноженная на нормировку даёт сам вектор: ||x|| · normalize(x) = x.

LaTeX

$$$\\|x\\|\\; \\cdot \\text{normalize}(x) = x$$$

Lean4

@[simp]
theorem norm_smul_normalize (x : V) : ‖x‖ • normalize x = x := by by_cases hx : x = 0 <;> simp [normalize, hx]

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

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

Разделы

Аффилиация

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