mk_univ_quaternion_of_infinite

Mathlib.Algebra.Quaternion

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

English

If R is infinite, the cardinality of the set-universal quaternion type equals the cardinality of R.

Русский

Если R бесконечно, кардинал Set.univ элементов ℍ[R] равен кардиналу R.

LaTeX

$$$|\mathrm{Set.univ} : \mathrm{Set}(\mathbb{H}(R))| = |R|$$$

Lean4

theorem mk_univ_quaternion_of_infinite [Infinite R] : #(Set.univ : Set ℍ[R]) = #R :=
  mk_univ_quaternionAlgebra_of_infinite _ _ _

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

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

Разделы

Аффилиация

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