inner_mul_symm_re_eq_norm — Mathlib

English

The real part of the product of inner products equals the norm of that product: Re (⟪x,y⟫ ⟪y,x⟫) = ‖⟪x,y⟫ ⟪y,x⟫‖.

Русский

Действительная часть произведения скалярных произведений равна норме этого произведения: Re (⟪x,y⟫ ⟪y,x⟫) = ‖⟪x,y⟫ ⟪y,x⟫‖.

LaTeX

$$$\operatorname{Re}\big( \langle x, y \rangle \langle y, x \rangle \big) = \| \langle x, y \rangle \langle y, x \rangle \|$$$

Lean4

theorem inner_mul_symm_re_eq_norm (x y : E) : re (⟪x, y⟫ * ⟪y, x⟫) = ‖⟪x, y⟫ * ⟪y, x⟫‖ :=
  by
  rw [← inner_conj_symm, mul_comm]
  exact re_eq_norm_of_mul_conj ⟪y, x⟫

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