inner_self_ofReal_re — Mathlib

English

The inner product ⟪x,x⟫ is real; equivalently, Re ⟪x,x⟫ = ⟪x,x⟫.

Русский

Скалярное произведение ⟪x,x⟫ вещественно; эквивалентно Re ⟪x,x⟫ = ⟪x,x⟫.

LaTeX

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

Lean4

@[simp]
theorem inner_self_ofReal_re (x : E) : (re ⟪x, x⟫ : 𝕜) = ⟪x, x⟫ :=
  ((RCLike.is_real_TFAE (⟪x, x⟫ : 𝕜)).out 2 3).2 (inner_self_im (𝕜 := 𝕜) x)

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