Local rings and residue fields

TheoremCharacteristic of the residue field of a local ring#✓fully proved

If (p : A) lies in the maximal ideal of a local ring A, the residue field has characteristic p: p maps to zero in the residue field.

theorem IsLocalRing.charP_residueField_of_natCast_mem_maximalIdeal
    (A : Type*) [CommRing A] [IsLocalRing A] (p : ℕ) [Fact p.Prime]
    (hAp : (p : A) ∈ IsLocalRing.maximalIdeal A) :
    CharP (IsLocalRing.ResidueField A) p

TheoremQuotient of a local ring by a proper ideal is local#✓fully proved

A quotient of a local ring by a proper ideal is local. Mathlib uses this fact inline (via IsLocalRing.of_surjective'), but does not package it as a standalone lemma.

theorem IsLocalRing.quotient_of_ne_top {A : Type*} [CommRing A] [IsLocalRing A]
    (I : Ideal A) (hI : I ≠ ⊤) : IsLocalRing (A ⧸ I)

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.