isNoetherianRing_iff_ideal_fg — Mathlib

English

A ring is Noetherian iff every ideal is finitely generated.

Русский

Кольцо Нётерово тогда и только тогда, когда каждый его идеал finitely generated.

LaTeX

$$$\\text{IsNoetherianRing}(R) \\iff \\forall I : \\text{Ideal } R, I.FG$$$

Lean4

/-- A ring is Noetherian if and only if all its ideals are finitely-generated. -/
theorem isNoetherianRing_iff_ideal_fg (R : Type*) [Semiring R] : IsNoetherianRing R ↔ ∀ I : Ideal R, I.FG :=
  isNoetherianRing_iff.trans isNoetherian_def

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