English
If 𝕜 is an RCLike field and E is a 𝕜-inner product space, then E carries a real inner product space structure by restricting scalars to ℝ, with inner on E given by ⟪x,y⟫_ℝ = Re ⟪x,y⟫_𝕜.
Русский
Пусть 𝕜 — поле RCLike, и E — 𝕜-внутреннее произведение. Тогда E наделяется структурой пространства с вещественным скалярным произведением путём ограничения скаляров до ℝ, скалярное произведение определяется как ⟪x,y⟫_ℝ = Re ⟪x,y⟫_𝕜.
LaTeX
$$$\\langle x,y\\rangle_{\\mathbb{R}} := \\operatorname{Re}\\langle x,y\\rangle_{\\mathbb{K}}.$$$
Lean4
/-- A general inner product space structure implies a real inner product structure.
This is not registered as an instance since
* `𝕜` does not appear in the return type `InnerProductSpace ℝ E`,
* It is likely to create instance diamonds, as it builds upon the diamond-prone
`NormedSpace.restrictScalars`.
However, it can be used in a proof to obtain a real inner product space structure from a given
`𝕜`-inner product space structure. -/
-- See note [reducible non-instances]
abbrev rclikeToReal : InnerProductSpace ℝ E :=
{ Inner.rclikeToReal 𝕜 E,
NormedSpace.restrictScalars ℝ 𝕜 E with
norm_sq_eq_re_inner := norm_sq_eq_re_inner
conj_inner_symm := fun _ _ => inner_re_symm _ _
add_left := fun x y z => by simp only [Inner.rclikeToReal, inner_add_left, map_add]
smul_left := fun x y r => by
letI := NormedSpace.restrictScalars ℝ 𝕜 E
have : r • x = (r : 𝕜) • x := rfl
simp only [Inner.rclikeToReal, this, conj_trivial, inner_smul_left, conj_ofReal, re_ofReal_mul] }
