ofQuaternion_comp_toQuaternion — Mathlib

English

There is an isomorphism of R-algebras between the Clifford algebra over Q c1 c2 and the quaternion algebra ℍ[R,c1,0,c2].

Русский

Существует изоморфизм R-алгебр между клиффордовой алгеброй над Q c1 c2 и кватернионной алгеброй ℍ[R,c1,0,c2].

LaTeX

$$$\mathrm{CliffordAlg}(Q(c_{1},c_{2})) \cong_{R} \mathbb{H}_{R}(c_{1},0,c_{2})$$$

Lean4

@[simp]
theorem ofQuaternion_comp_toQuaternion : ofQuaternion.comp toQuaternion = AlgHom.id R (CliffordAlgebra (Q c₁ c₂)) :=
  by
  ext : 1
  dsimp -- before we end up with two goals and have to do this twice

  ext
  all_goals
    dsimp
    rw [toQuaternion_ι]
    dsimp
    simp only [zero_smul, one_smul, zero_add, add_zero, RingHom.map_zero]

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