mathlib3

18b538a7 - feat(ring_theory/ideal/local_ring): add lemmas about and bundled versions of `local_ring.residue_field.map` (#17104)

feat(ring_theory/ideal/local_ring): add lemmas about and bundled versions of `local_ring.residue_field.map` (#17104) Add `local_ring.residue_field.map_id_apply` & `local_ring.residue_field.map_comp_apply` & ​`local_ring.residue_field.map_equiv`. Some more lemmata needed for the definition of inertia group. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>