isNoetherian_iff' — Mathlib

English

A module M is Noetherian if and only if every submodule is finitely generated.

Русский

Модуль M Ноетерен тогда и только тогда, когда каждый подмодуль конечноп порожден.

LaTeX

$$$IsNoetherian(R,M) \iff \forall s : Submodule(R,M), s.FG$$$

Lean4

theorem isNoetherian_iff' : IsNoetherian R M ↔ WellFoundedGT (Submodule R M) :=
  by
  refine .trans ?_ ((CompleteLattice.wellFoundedGT_characterisations <| Submodule R M).out 0 3).symm
  exact ⟨fun ⟨h⟩ => fun k => (fg_iff_compact k).mp (h k), fun h => ⟨fun k => (fg_iff_compact k).mpr (h k)⟩⟩

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