IsArtinian — Mathlib

English

Artinian property is defined as the well-foundedness of the submodule inclusion order.

Русский

Свойство артинности определяется как хорошо упорядоченность по включению подмодулей.

LaTeX

$$$\\mathrm{IsArtinian}(R,M) \\;\\Longleftrightarrow\\; \\mathrm{WellFounded}(\\,<\\, : \\mathrm{Submodule}_R M \\to \\mathrm{Submodule}_R M) $$$

Lean4

/-- `IsArtinian R M` is the proposition that `M` is an Artinian `R`-module,
implemented as the well-foundedness of submodule inclusion. -/
abbrev IsArtinian (R M) [Semiring R] [AddCommMonoid M] [Module R M] : Prop :=
  WellFoundedLT (Submodule R M)

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