instInnerProductSpaceRealComplex — Mathlib

English

The field 𝕜 in question is itself a real inner product space, with ⟨x,y⟩_ℝ = Re ⟨x,y⟩_𝕜 for x,y ∈ 𝕜.

Русский

Поле 𝕜 само является вещественным векторным пространством с внутренним произведением, задаваемым ⟨x,y⟩_ℝ = Re ⟨x,y⟩_𝕜 для x,y∈𝕜.

LaTeX

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

Lean4

instance : InnerProductSpace ℝ ℂ :=
  InnerProductSpace.complexToReal

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