ext — Mathlib

English

If two quaternions have equal real parts and equal imaginary components (imI, imJ, imK), then the quaternions are equal.

Русский

Если у двух кватернионов совпадают вещественные части и мнимые компоненты imI, imJ, imK, то кватернионы равны.

LaTeX

$$$$ \forall a,b \in \mathbb{H}(R),\ (a.re=b.re) \/ (a.imI=b.imI) \/ (a.imJ=b.imJ) \/ (a.imK=b.imK) \Rightarrow a=b. $$$$

Lean4

@[ext]
theorem ext : a.re = b.re → a.imI = b.imI → a.imJ = b.imJ → a.imK = b.imK → a = b :=
  QuaternionAlgebra.ext

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