isArtinian_iff — Mathlib

English

IsArtinian R M is equivalent to WellFounded on the lattice of submodules of M.

Русский

IsArtinian R M эквивалентно тому, что лемма подмодулей M образует WellFounded.

LaTeX

$$$\\mathrm{IsArtinian}~R~M \\leftrightarrow \\mathrm{WellFounded}(\\cdot < \\cdot : \\mathrm{Submodule}_R M \\to \\mathrm{Submodule}_R M) $$$

Lean4

theorem isArtinian_iff (R M) [Semiring R] [AddCommMonoid M] [Module R M] :
    IsArtinian R M ↔ WellFounded (· < · : Submodule R M → Submodule R M → Prop) :=
  isWellFounded_iff _ _

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