English
Let G be a real inner product space and f: G ≃ᵢℝ ℂ be a real-linear isomorphism. Then for all x,y ∈ G, ⟪x,y⟫ℝ = Re(f(y)·conj(f(x))).
Русский
Пусть G — вещественное пространство с скалярным произведением, и f: G ≃ᵢℝ ℂ — вещественно-линейное изоморфизм. Тогда для любых x,y ∈ G выполняется ⟪x,y⟫ℝ = Re(f(y)·conj(f(x))).
LaTeX
$$$⟪x,y⟫_ℝ = \operatorname{Re}\bigl( f y \cdot \overline{f x} \bigr)$$$
Lean4
/-- The inner product on an inner product space of dimension 2 can be evaluated in terms
of a complex-number representation of the space. -/
theorem inner_map_complex [SeminormedAddCommGroup G] [InnerProductSpace ℝ G] (f : G ≃ₗᵢ[ℝ] ℂ) (x y : G) :
⟪x, y⟫_ℝ = (f y * conj (f x)).re := by rw [← Complex.inner, f.inner_map_map]
