unitLattice_rank

Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

URI: https://scilib.ai/kg/mathlib#NumberField.Units.unitLattice_rank

English

The rank of the unit lattice equals the Dirichlet unit rank.

Русский

Ранг единичного решета равен рангу единиц Дирихле.

LaTeX

$$finrank_{\mathbb{Z}}(unitLattice(K)) = Units.rank(K)$$

Lean4

@[simp]
theorem unitLattice_rank : finrank ℤ (unitLattice K) = Units.rank K := by
  classical rw [← Units.finrank_eq_rank, ZLattice.rank ℝ]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru