eq_maximalIdeal

Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic

URI: https://scilib.ai/kg/mathlib#IsLocalRing.eq_maximalIdeal

← MathLib Explorer

English

If I is a maximal ideal, then I equals the maximal ideal of R.

Русский

Если I является максимальным идеалом, то I равно maximalIdeal R.

LaTeX

$$I.IsMaximal → I = maximalIdeal R$$

Lean4

theorem eq_maximalIdeal {I : Ideal R} (hI : I.IsMaximal) : I = maximalIdeal R :=
  ExistsUnique.unique (maximal_ideal_unique R) hI <| maximalIdeal.isMaximal R

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

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

Разделы

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

Аффилиация

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