isAtom

Mathlib.RingTheory.SimpleModule.Basic

URI: https://scilib.ai/kg/mathlib#IsSimpleModule.isAtom

English

If M is a simple R-module and m ≠ 0, then the kernel of the map toSpanSingleton R M m is a maximal ideal of R.

Русский

Если M — простой R-модуль и m ≠ 0, то ядро отображения toSpanSingleton R M m является максимальной идеалой R.

LaTeX

$$Ideal.IsMaximal (ker (toSpanSingleton R M m))$$

Lean4

@[simp]
theorem isAtom [IsSimpleModule R m] : IsAtom m :=
  isSimpleModule_iff_isAtom.1 ‹_›

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru