mathlib3
feat(group_theory/monoid_localization): some homs induced on localizations: lift, map
#2118
Merged
Merged