inner_self_re_eq_norm — Mathlib

English

The real part of ⟪x,x⟫ equals its norm: Re ⟪x,x⟫ = ‖⟪x,x⟫‖.

Русский

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

LaTeX

$$$\operatorname{Re} \langle x, x \rangle = \|\langle x, x \rangle\|$$$

Lean4

theorem inner_self_re_eq_norm (x : E) : re ⟪x, x⟫ = ‖⟪x, x⟫‖ :=
  by
  conv_rhs => rw [← inner_self_ofReal_re]
  symm
  exact norm_of_nonneg inner_self_nonneg

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