mem_fullyInvariantSubmodule_iff — Mathlib

English

For a submodule m of M, m is in the fully invariant submodule lattice if and only if m is fully invariant.

Русский

Подмодуль m лежит в системе полностью инвариантных подподмодулей тогда и только тогда, когда m полностью инвариантен.

LaTeX

$$$$ m \\in \\mathrm{fullyInvariantSubmodule}(R,M) \\iff m \\text{ IsFullyInvariant}. $$$$

Lean4

theorem mem_fullyInvariantSubmodule_iff {m : Submodule R M} : m ∈ fullyInvariantSubmodule R M ↔ m.IsFullyInvariant :=
  Iff.rfl

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