imK_mul — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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