isPrime_iff_isMaximal

Mathlib.RingTheory.Artinian.Module

URI: https://scilib.ai/kg/mathlib#IsArtinianRing.isPrime_iff_isMaximal

English

In an Artinian ring, an ideal is prime if and only if it is maximal.

Русский

В артиновом кольце идеал простой тогда, когда он максимальный.

LaTeX

$$$p \text{ prime} \iff p \text{ maximal}$$$

Lean4

theorem isPrime_iff_isMaximal (p : Ideal R) : p.IsPrime ↔ p.IsMaximal :=
  ⟨fun _ ↦ isMaximal_of_isPrime p, fun h ↦ h.isPrime⟩

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

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

Разделы

Аффилиация

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