equivTuple — Mathlib

English

There is an isomorphism between the quaternion algebra ℍ[R,c1,c2,c3] and the function space Fin 4 → R.

Русский

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

LaTeX

$$$\ℍ[R,c_1,c_2,c_3] \cong (\mathrm{Fin}\ 4 \to R)$$$

Lean4

/-- The equivalence between a quaternion algebra over `R` and `Fin 4 → R`. -/
@[simps symm_apply]
def equivTuple {R : Type*} (c₁ c₂ c₃ : R) : ℍ[R,c₁,c₂,c₃] ≃ (Fin 4 → R)
    where
  toFun a := ![a.1, a.2, a.3, a.4]
  invFun a := ⟨a 0, a 1, a 2, a 3⟩
  right_inv _ := by ext ⟨_, _ | _ | _ | _ | _ | ⟨⟩⟩ <;> rfl

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