setOf_isMaximal_finite — Mathlib

English

In an Artinian ring, the set of maximal ideals is finite.

Русский

В артиновом кольце множество максимиальных идеалов конечное.

LaTeX

$$$\{ I \mid I \text{ maximal in } R \} \text{ is finite }$$$

Lean4

@[stacks 00J7]
theorem setOf_isMaximal_finite : {I : Ideal R | I.IsMaximal}.Finite :=
  by
  have ⟨s, H⟩ := Finset.exists_inf_le (Subtype.val (p := fun I : Ideal R ↦ I.IsMaximal))
  refine Set.finite_def.2 ⟨s, fun p ↦ ?_⟩
  have ⟨q, hq1, hq2⟩ := p.2.isPrime.inf_le'.mp (H p)
  rwa [← Subtype.ext <| q.2.eq_of_le p.2.ne_top hq2]

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