imI_mul — Mathlib

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

Похожие утверждения