English
The quaternion algebra ℍ[R,c1,c2,c3] has the same cardinality as the fourfold product R^4; that is, there exists a bijection between ℍ[R,c1,c2,c3] and R^4.
Русский
Кватернионная алгебра над кольцом R с параметрами c₁,c₂,c₃ имеет кардинальность, равную кардинальности R^4; существует биекция между ℍ[R,c₁,c₂,c₃] и R^4.
LaTeX
$$$\#\Big(\mathbb{H}(R,c_1,c_2,c_3)\Big) = \big(\#R\big)^4$$$
Lean4
/-- The cardinality of a quaternion algebra, as a type. -/
theorem mk_quaternionAlgebra : #(ℍ[R,c₁,c₂,c₃]) = #R ^ 4 :=
by
rw [mk_congr (QuaternionAlgebra.equivProd c₁ c₂ c₃)]
simp only [mk_prod, lift_id]
ring