Commit 2019-03-06 14:21 cc753d7b
View on Github →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