mk_quaternionAlgebra — Mathlib

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

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