maximalIdeal_eq_bot

Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic

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

← MathLib Explorer

English

In a field, the maximal ideal is the bottom (zero) submodule.

Русский

В поле максимальный идеал — нулевой подмодуль.

LaTeX

$$$ \operatorname{maximalIdeal}(R) = ⊥. $$$

Lean4

theorem maximalIdeal_eq_bot {R : Type*} [Field R] : IsLocalRing.maximalIdeal R = ⊥ :=
  IsLocalRing.isField_iff_maximalIdeal_eq.mp (Field.toIsField R)

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

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

Разделы

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

Аффилиация

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