re_mul — Mathlib

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]

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