inner_self_im — Mathlib

English

Let F be a complex inner product space. Then the imaginary part of the inner product of any vector with itself is zero: Im ⟪x, x⟫ = 0 for all x ∈ F.

Русский

Пусть F — комплексное пространство с вложенным скалярным произведением. Тогда мнимая часть скалярного произведения вектора с самим собой равна нулю: Im ⟪x, x⟫ = 0 для всех x ∈ F.

LaTeX

$$$\operatorname{Im}\langle x, x\rangle = 0$$$

Lean4

theorem inner_self_im (x : F) : im ⟪x, x⟫ = 0 :=
  by
  rw [← @ofReal_inj 𝕜, im_eq_conj_sub]
  simp [inner_conj_symm]

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