complexToReal — Mathlib

English

If G is a complex inner product space, then there is a real inner product space structure on G given by ⟪x,y⟫_ℝ := Re ⟪x,y⟫_ℂ.

Русский

Если G — комплексное пространство с внутренним произведением, то на G задают вещественное скалярное произведение ⟪x,y⟫_ℝ := Re ⟪x,y⟫_ℂ.

LaTeX

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

Lean4

/-- A complex inner product implies a real inner product. This cannot be an instance since it
creates a diamond with `PiLp.innerProductSpace` because `re (sum i, ⟪x i, y i⟫)` and
`sum i, re ⟪x i, y i⟫` are not defeq. -/
def complexToReal [SeminormedAddCommGroup G] [InnerProductSpace ℂ G] : InnerProductSpace ℝ G :=
  InnerProductSpace.rclikeToReal ℂ G

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