English
Any RCLike field 𝕜 carries a real inner product space structure on itself, with ⟨x,y⟩_ℝ = Re ⟨x,y⟩_𝕜.
Русский
Любое поле RCLike 𝕜 обладает структурой пространства с вещественным внутренним произведением на себе, задаваемым ⟨x,y⟩_ℝ = Re ⟨x,y⟩_𝕜.
LaTeX
$$$\\langle x,y\\rangle_{\\mathbb{R}} = \\operatorname{Re}\\langle x,y\\rangle_{\\mathbb{K}}\\quad (x,y\\in 𝕜).$$$
Lean4
/-- An `RCLike` field is a real inner product space. -/
noncomputable instance toInnerProductSpaceReal : InnerProductSpace ℝ 𝕜
where
__ := Inner.rclikeToReal 𝕜 𝕜
norm_sq_eq_re_inner := norm_sq_eq_re_inner
conj_inner_symm x y := inner_re_symm ..
add_left x y z := show re (_ * _) = re (_ * _) + re (_ * _) by simp only [map_add, mul_re, conj_re, conj_im]; ring
smul_left x y
r :=
show re (_ * _) = _ * re (_ * _) by simp only [mul_re, conj_re, conj_im, conj_trivial, smul_re, smul_im];
ring
-- The instance above does not create diamonds for concrete `𝕜`:
