equivTuple — Mathlib

English

Let R be a ring. There is an algebra isomorphism between the quaternions over R and the space of functions Fin(4) → R.

Русский

Пусть R — кольцо. Существует изоморфизм алгебр между ℍ(R) и пространством функций Fin(4) → R.

LaTeX

$$$$\mathbb{H}(R) \cong (\mathrm{Fin}(4) \to R).$$$$

Lean4

/-- The equivalence between the quaternions over `R` and `Fin 4 → R`. -/
@[simps! symm_apply]
def equivTuple (R : Type*) [Zero R] [One R] [Neg R] : ℍ[R] ≃ (Fin 4 → R) :=
  QuaternionAlgebra.equivTuple _ _ _

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