mathlib3

bbcc67f5 - feat(ring_theory/ideal/local_ring): add ​local_ring.residue_field.map_id & local_ring.residue_field.map_comp (#16916)

feat(ring_theory/ideal/local_ring): add ​local_ring.residue_field.map_id & local_ring.residue_field.map_comp (#16916) Applying `map` to the identity ring homomorphism gives the identity ring homomorphism. The composite of two `map`s is the `map` of the composite. I need these for my study of the inertia group Co-authored-by: mkaratarakis <40603357+mkaratarakis@users.noreply.github.com>