equivProd — Mathlib

English

There is an isomorphism between a quaternion algebra ℍ[R,c1,c2,c3] and the product ring R × R × R × R.

Русский

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

LaTeX

$$$\ℍ[R,c_1,c_2,c_3] \cong R \times R \times R \times R$$$

Lean4

/-- The equivalence between a quaternion algebra over `R` and `R × R × R × R`. -/
@[simps]
def equivProd {R : Type*} (c₁ c₂ c₃ : R) : ℍ[R,c₁,c₂,c₃] ≃ R × R × R × R
    where
  toFun a := ⟨a.1, a.2, a.3, a.4⟩
  invFun a := ⟨a.1, a.2.1, a.2.2.1, a.2.2.2⟩

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