Commit 2021-06-09 06:11 393f6389
View on Github →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.