finrank_eq_four

Mathlib.Algebra.Quaternion

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

English

Under Strong Rank Condition, the finite rank of the quaternion algebra over R is 4.

Русский

При условии сильного рангового условия конечный размер квадрантов кватернионной алгебры над R равен 4.

LaTeX

$$$ Module.finrank_R(\\mathbb{H}(R)) = 4 $$$

Lean4

theorem finrank_eq_four [StrongRankCondition R] : Module.finrank R ℍ[R] = 4 :=
  QuaternionAlgebra.finrank_eq_four _ _ _

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

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

Разделы

Аффилиация

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