isMaximal

Mathlib.RingTheory.DedekindDomain.Basic

URI: https://scilib.ai/kg/mathlib#Ideal.IsPrime.isMaximal

← MathLib Explorer

English

In a ring of dimension ≤ 1, every nonzero prime ideal is maximal.

Русский

В кольце размерности ≤ 1 каждый ненулевой простый идеал максимален.

LaTeX

$$p.IsPrime → p.IsMaximal$$

Lean4

theorem isMaximal {R : Type*} [CommRing R] [DimensionLEOne R] {p : Ideal R} (h : p.IsPrime) (hp : p ≠ ⊥) :
    p.IsMaximal :=
  DimensionLEOne.maximalOfPrime hp h

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

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

Разделы

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

Аффилиация

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