real_inner_eq_re_inner — Mathlib

English

For all x,y in E, the real inner product satisfies ⟪x,y⟫_ℝ = Re ⟪x,y⟫_𝕜.

Русский

Для любых x,y ∈ E вещественное скалярное произведение удовлетворяет ⟪x,y⟫_ℝ = Re ⟪x,y⟫_𝕜.

LaTeX

$$$\\langle x,y\\rangle_{\\mathbb{R}} = \\operatorname{Re}\\langle x,y\\rangle_{\\mathbb{K}}.$$$

Lean4

theorem real_inner_eq_re_inner (x y : E) : (Inner.rclikeToReal 𝕜 E).inner x y = re ⟪x, y⟫ :=
  rfl

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