mathlib3

758a6a4e - feat(ring_theory/ideal/local_ring): add lemmas about local_ring.residue_field.map (#17969)

feat(ring_theory/ideal/local_ring): add lemmas about local_ring.residue_field.map (#17969) Add `map_comp_residue` & `map_residue` in `residue_field.map`. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>