mk_univ_quaternionAlgebra_of_infinite

Mathlib.Algebra.Quaternion

URI: https://scilib.ai/kg/mathlib#Cardinal.mk_univ_quaternionAlgebra_of_infinite

English

If R is infinite, the cardinality of the quaternion algebra equals the cardinality of R.

Русский

Если R бесконечно, кардинал кватернионной алгебры равен кардиналу R.

LaTeX

$$$|\mathbb{H}(R,c_1,c_2,c_3)| = |R|\quad (\text{if } |R| = \infty)$$$

Lean4

theorem mk_univ_quaternionAlgebra_of_infinite [Infinite R] : #(Set.univ : Set ℍ[R,c₁,c₂,c₃]) = #R := by
  rw [mk_univ_quaternionAlgebra, pow_four]

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

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

Разделы

Аффилиация

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