ne_bot_of_isMaximal_of_not_isField

English

If R is not a field, then every maximal ideal M is nontrivial, i.e., M ≠ ⊥.

Русский

Если кольцо не является полем, то любой максимальный идеал не тривиален, то есть M ≠ ⊥.

LaTeX

$$$\\forall M:\\mathrm{Ideal}(R),\\ M\\text{ maximal }\\Rightarrow \\neg\\mathrm{IsField}(R)\\rightarrow M \\neq \\bot$$$

Lean4

/-- When a ring is not a field, the maximal ideals are nontrivial. -/
theorem ne_bot_of_isMaximal_of_not_isField [Nontrivial R] {M : Ideal R} (max : M.IsMaximal) (not_field : ¬IsField R) :
    M ≠ ⊥ := by
  rintro h
  rw [h] at max
  rcases max with ⟨⟨_h1, h2⟩⟩
  obtain ⟨I, hIbot, hItop⟩ := not_isField_iff_exists_ideal_bot_lt_and_lt_top.mp not_field
  exact ne_of_lt hItop (h2 I hIbot)

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