inner_self_eq_norm_sq

Mathlib.Analysis.InnerProductSpace.Basic

URI: https://scilib.ai/kg/mathlib#inner_self_eq_norm_sq

English

If ∀ v, ⟪v, x⟫ = ⟪v, y⟫, then x = y.

Русский

Если ∀ v: ⟪v, x⟫ = ⟪v, y⟫, то x = y.

LaTeX

$$∀ v, ⟪v, x⟫ = ⟪v, y⟫ → x = y$$

Lean4

theorem inner_self_eq_norm_sq (x : E) : re ⟪x, x⟫ = ‖x‖ ^ 2 := by rw [pow_two, inner_self_eq_norm_mul_norm]

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

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

Разделы

Аффилиация

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