isSimpleModule_iff_isAtom — Mathlib

English

For a submodule m of M, the R-module m is simple iff m is an atom in the lattice of submodules of M.

Русский

Для подмодуля m модуля M модуль R простой тогда и только тогда, когда m является атомом в решетке подмодулей M.

LaTeX

$$$\\text{IsSimpleModule } R m \\;\\iff\\; \\text{IsAtom } m$$$

Lean4

theorem isSimpleModule_iff_isAtom : IsSimpleModule R m ↔ IsAtom m :=
  by
  rw [← Set.isSimpleOrder_Iic_iff_isAtom, isSimpleModule_iff]
  exact m.mapIic.isSimpleOrder_iff

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