instFinite

Mathlib.Algebra.Quaternion

URI: https://scilib.ai/kg/mathlib#QuaternionAlgebra.instFinite

English

The quaternion algebra ℍ[R,c1,c2,c3] is a finite module over R with a basis basisOneIJK.

Русский

Кватернионная алгебра ℍ[R,c1,c2,c3] является конечным модулем над R с базисом basisOneIJK.

LaTeX

$$$\mathbb{H}(R;c_1,c_2,c_3) \text{ is a finite } R\text{-module with basis } basisOneIJK.$$$

Lean4

instance : Module.Finite R ℍ[R,c₁,c₂,c₃] :=
  .of_basis (basisOneIJK c₁ c₂ c₃)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru