exists_le_maximal — Mathlib

English

If I is a proper ideal, there exists a maximal ideal M containing I.

Русский

Если I — правильный идеал, существует максимальный идеал M, содержащий I.

LaTeX

$$$I \neq \top \Rightarrow \exists M:\ Ideal\ α, M.IsMaximal \land I \le M$$$

Lean4

/-- **Krull's theorem**: if `I` is an ideal that is not the whole ring, then it is included in some
    maximal ideal. -/
theorem exists_le_maximal (I : Ideal α) (hI : I ≠ ⊤) : ∃ M : Ideal α, M.IsMaximal ∧ I ≤ M :=
  let ⟨m, hm⟩ := (eq_top_or_exists_le_coatom I).resolve_left hI
  ⟨m, ⟨⟨hm.1⟩, hm.2⟩⟩

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