isNoetherian_iff — Mathlib

English

An equivalence describing Noetherian property of a fractional ideal in terms of all sub-ideals within it being finitely generated.

Русский

Эквивалентность: дробный идеал является Неотерминируемым тогда и только тогда, все подпредметы внутри него конечнопорождены.

LaTeX

$$IsNoetherian R₁ I ↔ ∀ J ≤ I, (J : Submodule R₁ K).FG$$

Lean4

theorem isNoetherian_iff {I : FractionalIdeal R₁⁰ K} : IsNoetherian R₁ I ↔ ∀ J ≤ I, (J : Submodule R₁ K).FG :=
  isNoetherian_submodule.trans ⟨fun h _ hJ => h _ hJ, fun h J hJ => h ⟨J, isFractional_of_le hJ⟩ hJ⟩

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