Commit 2024-12-20 14:09 83682ff2

View on Github →

feat(RingTheory): the residue field of a prime ideal (#18416)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/LocalRing/ResidueField/Ideal.lean

added def Ideal.ResidueField.mapₐ

added theorem Ideal.ResidueField.mapₐ_apply

added theorem Ideal.algebraMap_residueField_eq_zero

added theorem Ideal.bijective_algebraMap_quotient_residueField

added theorem Ideal.injective_algebraMap_quotient_residueField

added theorem Ideal.ker_algebraMap_residueField

added theorem algebraMap_mk