feat(ring_theory/localization): adds induced ring hom between fraction rings (#781)
feat(ring_theory/localization): adds induced ring hom between fraction rings (#781)

* feat(ring_theory/localization): adds induced ring hom between fraction rings

* Break some extremely long lines

* Put map in the fraction_ring namespace

* Move global variable into statements

* Rename rec to lift', make interface for lift, generalise map

* Improve simp-lemmas, add docstrings

* Rename circ to comp in lemma names

leanprover-community/mathlib,leanprover-community/mathlib