English
The real part of a product expands to the standard quaternion real part formula: Re(a b) = a.re b.re − a.imI b.imI − a.imJ b.imJ − a.imK b.imK.
Русский
Действительная часть произведения раскладывается по стандартной формуле кватерниона: Re(a b) = a.re b.re − a.imI b.imI − a.imJ b.imJ − a.imK b.imK.
LaTeX
$$$ (a * b).re = a.re * b.re - a.imI * b.imI - a.imJ * b.imJ - a.imK * b.imK $$$
Lean4
@[simp]
theorem re_mul : (a * b).re = a.re * b.re - a.imI * b.imI - a.imJ * b.imJ - a.imK * b.imK :=
(QuaternionAlgebra.re_mul a b).trans <| by simp [one_mul, neg_mul, sub_eq_add_neg, neg_neg]