mathlib3

cc753d7b - 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