basisOneIJK — Mathlib

English

Over R, the quaternion algebra ℍ[R,c1,c2,c3] is a free module with basis 1, i, j, k, i.e., a basis indexed by Fin 4 corresponds to {1,i,j,k}.

Русский

Кватернионная алгебра ℍ[R,c1,c2,c3] является свободным модулем над R с базисом 1, i, j, k (индексированным Fin 4).

LaTeX

$$$\text{basisOneIJK} : \text{Basis} (\mathrm{Fin}\,4)\, R\, \mathbb{H}(R;c_1,c_2,c_3).$$$

Lean4

/-- `ℍ[R, c₁, c₂, c₃]` has a basis over `R` given by `1`, `i`, `j`, and `k`. -/
noncomputable def basisOneIJK : Basis (Fin 4) R ℍ[R,c₁,c₂,c₃] :=
  .ofEquivFun <| linearEquivTuple c₁ c₂ c₃

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