toQuaternion_ofQuaternion — Mathlib

English

The other direction of the isomorphism asserts that applying ofQuaternion to a quaternion and then toQuaternion returns the original quaternion.

Русский

Применение ofQuaternion к кватерниону, затем toQuaternion возвращает исходный кватернион.

LaTeX

$$$\bigl(\,ofQuaternion \circ toQuaternion\bigr)(c) = c$ for all $c \in \mathrm{CliffordAlg}(Q(c_{1},c_{2}))$$$

Lean4

@[simp]
theorem toQuaternion_ofQuaternion (q : ℍ[R,c₁,0,c₂]) : toQuaternion (ofQuaternion q) = q :=
  AlgHom.congr_fun toQuaternion_comp_ofQuaternion q

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