instIsNoetherianInt

Mathlib.NumberTheory.NumberField.Basic

URI: https://scilib.ai/kg/mathlib#NumberField.RingOfIntegers.instIsNoetherianInt

English

𝓞_K is a Noetherian ℤ-module (in fact a finitely generated free ℤ-module).

Русский

𝓞_K является Noetherian ℤ-модулем; на самом деле свободным ℤ-модулем конечного ранга.

LaTeX

$$$\\mathcal{O}_K\\ \\text{is a Noetherian }\\mathbb{Z}-\\text{module}$$$

Lean4

instance : IsNoetherian ℤ (𝓞 K) :=
  IsIntegralClosure.isNoetherian _ ℚ K _

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

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

Разделы

Аффилиация

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