rank_modTorsion — Mathlib

English

The rank of the unit quotient equals the base field rank (Dirichlet theorem).

Русский

Ранг квота единиц равен рангу поля (теорема Дирихле).

LaTeX

$$Module.finrank Int (Additive ((HasQuotient.Quotient (Units (NumberField.RingOfIntegers K)) (NumberField.Units.torsion K)))) = rank K$$

Lean4

theorem rank_modTorsion : Module.finrank ℤ (Additive ((𝓞 K)ˣ ⧸ (torsion K))) = rank K := by
  rw [← LinearEquiv.finrank_eq (logEmbeddingEquiv K).symm, unitLattice_rank]

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