mathlib3

393f6389 - feat(ring_theory/localization): Make local_ring_hom more flexible (#7787)

feat(ring_theory/localization): Make local_ring_hom more flexible (#7787) Make `localization.local_ring_hom` more flexible, by allowing two ideals `I` and `J` as arguments, with the assumption that `I` equals `ideal.comap f J`. Also add lemmas about identity and composition.