instIsAtomicOfIsArtinian — Mathlib

English

If M is Artinian, then LieSubmodule R L M is atomic (every nonzero submodule contains an atom).

Русский

Если M-Artinian, то Ли-подмодульная решётка атомарна: каждый ненулевой подмодуль содержит атом.

LaTeX

$$IsArtinian R M \\Rightarrow IsAtomic (LieSubmodule R L M)$$

Lean4

instance [IsArtinian R M] : IsAtomic (LieSubmodule R L M) :=
  isAtomic_of_orderBot_wellFounded_lt <| (wellFoundedLT_of_isArtinian R L M).wf

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