imJ_mul — Mathlib

English

The J-imaginary component of a product is given by ImJ(a b) = a.re b.imJ − a.imI b.imK + a.imJ b.re + a.imK b.imI.

Русский

Компонента imJ произведения: ImJ(a b) = a.re b.imJ − a.imI b.imK + a.imJ b.re + a.imK b.imI.

LaTeX

$$$ (a * b).imJ = a.re * b.imJ - a.imI * b.imK + a.imJ * b.re + a.imK * b.imI $$$

Lean4

@[simp]
theorem imJ_mul : (a * b).imJ = a.re * b.imJ - a.imI * b.imK + a.imJ * b.re + a.imK * b.imI :=
  (QuaternionAlgebra.imJ_mul a b).trans <| by ring

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