bot_lt_of_maximal — Mathlib

English

If R is not a field and M is maximal, then ⊥ < M.

Русский

Если R не является полем и M — максимальный идеал, то ⊥ < M.

LaTeX

$$$\\bot < M$$$

Lean4

theorem bot_lt_of_maximal (M : Ideal R) [hm : M.IsMaximal] (non_field : ¬IsField R) : ⊥ < M :=
  by
  rcases Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top.1 non_field with ⟨I, Ibot, Itop⟩
  constructor; · simp
  intro mle
  apply lt_irrefl (⊤ : Ideal R)
  have : M = ⊥ := eq_bot_iff.mpr mle
  rw [← this] at Ibot
  rwa [hm.1.2 I Ibot] at Itop

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