isMaximal — Mathlib

English

In a local ring, the maximal ideal is a maximal ideal.

Русский

В локальном кольце максимальный идеал является максимальным идеалом.

LaTeX

$$IsLocalRing.maximalIdeal.isMaximal$$

Lean4

instance isMaximal : (maximalIdeal R).IsMaximal :=
  by
  rw [Ideal.isMaximal_iff]
  constructor
  · intro h
    apply h
    exact isUnit_one
  · intro I x _ hx H
    rw [mem_maximalIdeal, mem_nonunits_iff, Classical.not_not] at hx
    rcases hx with ⟨u, rfl⟩
    simpa using I.mul_mem_left (↑u⁻¹) H

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