English
The I-imaginary component of a product is given by ImI(a b) = a.re b.imI + a.imI b.re + a.imJ b.imK − a.imK b.imJ.
Русский
Компонента imI произведения равна ImI(a b) = a.re b.imI + a.imI b.re + a.imJ b.imK − a.imK b.imJ.
LaTeX
$$$ (a * b).imI = a.re * b.imI + a.imI * b.re + a.imJ * b.imK - a.imK * b.imJ $$$
Lean4
@[simp]
theorem imI_mul : (a * b).imI = a.re * b.imI + a.imI * b.re + a.imJ * b.imK - a.imK * b.imJ :=
(QuaternionAlgebra.imI_mul a b).trans <| by ring