isMaximal_of_isPrime

Mathlib.RingTheory.Artinian.Module

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

← MathLib Explorer

English

In an Artinian ring, every prime ideal is maximal.

Русский

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

LaTeX

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

Lean4

instance isMaximal_of_isPrime {R : Type*} [CommRing R] (p : Ideal R) [p.IsPrime] [IsArtinianRing R] : p.IsMaximal :=
  Ideal.Quotient.maximal_of_isField _ (isField_of_isDomain _)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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