English
The kahler product with a is multiplicative: o.kahler x a · o.kahler a y = ||a||^2 · o.kahler x y.
Русский
Произведение kahler по середине: o.kahler x a · o.kahler a y = ||a||^2 · o.kahler x y.
LaTeX
$$o.kahler x a \\cdot o.kahler a y = ||a||^2 \\cdot o.kahler x y$$
Lean4
theorem kahler_mul (a x y : E) : o.kahler x a * o.kahler a y = ‖a‖ ^ 2 * o.kahler x y :=
by
trans ((‖a‖ ^ 2 :) : ℂ) * o.kahler x y
· apply Complex.ext
· simp only [o.kahler_apply_apply, Complex.add_im, Complex.add_re, Complex.I_im, Complex.I_re, Complex.mul_im,
Complex.mul_re, Complex.ofReal_im, Complex.ofReal_re, Complex.real_smul]
rw [real_inner_comm a x, o.areaForm_swap x a]
linear_combination o.inner_mul_inner_add_areaForm_mul_areaForm a x y
· simp only [o.kahler_apply_apply, Complex.add_im, Complex.add_re, Complex.I_im, Complex.I_re, Complex.mul_im,
Complex.mul_re, Complex.ofReal_im, Complex.ofReal_re, Complex.real_smul]
rw [real_inner_comm a x, o.areaForm_swap x a]
linear_combination o.inner_mul_areaForm_sub a x y
· norm_cast
