isMaximal_iff — Mathlib

English

A is maximal iff A = maximalIdeal R in a local ring.

Русский

Крайний идеал A максимален тогда и только тогда, когда A = maximalIdeal R в локальном кольце.

LaTeX

$$theorem isMaximal_iff {I : Ideal R} : I.IsMaximal ↔ I = maximalIdeal R$$

Lean4

theorem isMaximal_iff {I : Ideal R} : I.IsMaximal ↔ I = maximalIdeal R
    where
  mp hI := hI.eq_of_le (maximalIdeal.isMaximal R).1.1 fun _ h ↦ hI.1.1 ∘ I.eq_top_of_isUnit_mem h
  mpr e := e ▸ maximalIdeal.isMaximal R

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