Theorem Ideal.bijective_algebraMap_quotient_residueField

Modification history

2024-12-20 14:09
Mathlib/RingTheory/LocalRing/ResidueField/Ideal.lean
feat(RingTheory): the residue field of a prime ideal (#18416)
Added Ideal.bijective_algebraMap_quotient_residueFieldView on Github →