instFinite

Mathlib.Algebra.Quaternion

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

English

The quaternion algebra ℍ[R] is a finitely generated module over R.

Русский

Алгебра кватернионов ℍ[R] является конечно порожденным модулем над R.

LaTeX

$$$ Module.Finite\, R\, \\mathbb{H}(R) $$$

Lean4

instance : Module.Finite R ℍ[R] :=
  inferInstanceAs <| Module.Finite R ℍ[R,-1,0,-1]

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

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

Разделы

Аффилиация

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