Theorems · Definition · commutative algebra

Ideal.ResidueField

{R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → [I.IsPrime] → Type u_1

The residue field at a prime ideal, defined to be the residue field of the local ring Localization.Prime I. We also provide an IsFractionRing (R ⧸ I) I.ResidueField instance.

Defined in

Mathlib.RingTheory.LocalRing.ResidueField.Ideal

Cited by

119 results in Mathlib

Foundations

Depth 72 from the axioms, rests on 1,364 definitions · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIdeal.IsPrime