isNoetherian_submodule_right — Mathlib

English

The Noetherian property can be characterized via intersections with any submodule: (N ⊓ s).FG for all s.

Русский

Свойство Ноетерова может быть охарактеризовано через пересечения с любым подмодулем: (N ⊓ s).FG для всех s.

LaTeX

$$$IsNoetherian(R,N) \iff ∀ s, (s \cap N).FG$$$

Lean4

theorem isNoetherian_submodule_right {N : Submodule R M} : IsNoetherian R N ↔ ∀ s : Submodule R M, (s ⊓ N).FG :=
  isNoetherian_submodule.trans ⟨fun H _ => H _ inf_le_right, fun H _ hs => inf_of_le_left hs ▸ H _⟩

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