instFree

Mathlib.Algebra.Quaternion

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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