rank_eq_four — Mathlib

English

If R satisfies StrongRankCondition, then the rank of the quaternion algebra as an R-module is 4.

Русский

При наличии условия StrongRankCondition на R размерность кватернионной алгебры как модуля над R равна 4.

LaTeX

$$$\text{rank}_R \mathbb{H}(R;c_1,c_2,c_3) = 4.$$$

Lean4

theorem rank_eq_four [StrongRankCondition R] : Module.rank R ℍ[R,c₁,c₂,c₃] = 4 :=
  by
  rw [rank_eq_card_basis (basisOneIJK c₁ c₂ c₃), Fintype.card_fin]
  norm_num

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