norm_zero

Mathlib.Analysis.CStarAlgebra.Module.Defs

URI: https://scilib.ai/kg/mathlib#CStarModule.norm_zero

English

The norm of the zero vector is zero: ||0|| = 0.

Русский

Норма нулевого вектора равна нулю: ||0|| = 0.

LaTeX

$$$\\\\|0_E\\\\| = 0$$$

Lean4

protected theorem norm_zero : ‖(0 : E)‖ = 0 := by simp [norm_eq_sqrt_norm_inner_self (A := A)]

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

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

Разделы

Аффилиация

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