toQuaternion_comp_ofQuaternion — Mathlib

English

The composition of the two maps to and from the quaternion algebra yields the identity on the quaternion algebra, i.e., toQuaternion ∘ ofQuaternion = id on ℍ[R,c1,0,c2].

Русский

Композиция обратных отображений между кватернионной и клиффордовой алгебрами равна тождественному отображению на ℍ[R,c1,0,c2].

LaTeX

$$$\bigl(\,toQuaternion \circ ofQuaternion\bigr) = \mathrm{id}_{\mathbb{H}_{R}(c_{1},0,c_{2})}$$$

Lean4

@[simp]
theorem toQuaternion_comp_ofQuaternion : toQuaternion.comp ofQuaternion = AlgHom.id R ℍ[R,c₁,0,c₂] := by
  ext : 1 <;> simp

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