mk_univ_quaternionAlgebra — Mathlib

English

The cardinality of the quaternion algebra as a set is the same as the cardinality of R^4, reflecting a natural identification with R^4.

Русский

Кардинал множества кватернионной алгебры совпадает с кардиналом R^4, отражая естественное соответствие с R^4.

LaTeX

$$$|\{ x : \mathbb{H}(R,c_1,c_2,c_3) \}| = |R|^{4}$$$

Lean4

/-- The cardinality of a quaternion algebra, as a set. -/
theorem mk_univ_quaternionAlgebra : #(Set.univ : Set ℍ[R,c₁,c₂,c₃]) = #R ^ 4 := by rw [mk_univ, mk_quaternionAlgebra]

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