instFGUnitsRingOfIntegers

Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

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

English

The units of the ring of integers form a finitely generated abelian group.

Русский

Единицы кольца целых чисел образуют конечнопорождённую абелеву группу.

LaTeX

$$Monoid.FG (Units (NumberField.RingOfIntegers K))$$

Lean4

instance : Monoid.FG (𝓞 K)ˣ :=
  by
  rw [Monoid.fg_iff_add_fg, ← AddGroup.fg_iff_addMonoid_fg, ← Module.Finite.iff_addGroup_fg]
  infer_instance

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

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

Разделы

Аффилиация

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