English
Let E be a vector space with a 𝕜-inner product for some RCLike field 𝕜. Define ⟪x,y⟫_ℝ := Re ⟪x,y⟫. Then ⟪·,·⟫_ℝ is a real inner product on E, giving E the structure of an inner product space over ℝ.
Русский
Пусть E — векторное пространство, снабжённое 𝕜-внутренним произведением для некоторого поля 𝕜, являющегося RCLike. Определим ⟪x,y⟫_ℝ := Re ⟪x,y⟫. Тогда ⟪·,·⟫_ℝ является вещественным скалярным произведением на E, и E приобретает структуру пространства с вещественным скалярным произведением.
LaTeX
$$$\\langle x,y\\rangle_{\\mathbb{R}} := \\operatorname{Re}\\langle x,y\\rangle_{\\mathbb{K}}.$$$
Lean4
/-- A general inner product implies a real inner product. This is not registered as an instance
since `𝕜` does not appear in the return type `Inner ℝ E`. -/
def rclikeToReal : Inner ℝ E where inner x y := re ⟪x, y⟫
