le_maximalIdeal

Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic

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

← MathLib Explorer

English

If J is a proper ideal (not equal to⊤), then J ≤ maximalIdeal R.

Русский

Если J — корректный идеал (не равен ⊤), то J ⊆ maximalIdeal R.

LaTeX

$$le_maximalIdeal: ∀ {J : Ideal R}, J ≠ ⊤ → J ≤ maximalIdeal R$$

Lean4

theorem le_maximalIdeal {J : Ideal R} (hJ : J ≠ ⊤) : J ≤ maximalIdeal R :=
  by
  rcases Ideal.exists_le_maximal J hJ with ⟨M, hM1, hM2⟩
  rwa [← eq_maximalIdeal hM1]

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

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

Разделы

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

Аффилиация

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