instIsNoetherianSubtypeMem — Mathlib

English

If M is Artinian as an R-module, then any LieSubmodule N of M is Artinian as an R-module (via underlying Submodule).

Русский

Если M артинов по модулю R, то любой LieSubmodule N M артинов по модулю R через подмодуль.

LaTeX

$$∀ {R L M} [IsArtinian R M] (N : LieSubmodule R L M), IsArtinian R N$$

Lean4

instance [IsNoetherian R M] (N : LieSubmodule R L M) : IsNoetherian R N :=
  inferInstanceAs <| IsNoetherian R N.toSubmodule

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