mathlib3
feat(ring_theory/localization): adds induced ring hom between fraction rings
#781
Merged
Merged
feat(ring_theory/localization): adds induced ring hom between fraction rings #781
ChrisHughes24
merged
9 commits into
master
from
fraction-ring-map
feat(ring_theory/localization): adds induced ring hom between fractio…
15c4478f
Break some extremely long lines
92153bbd
Put map in the fraction_ring namespace
e3a12f8e
Move global variable into statements
69bc1c0d
Merge branch 'master' into fraction-ring-map
7b3cd0c1
Rename rec to lift', make interface for lift, generalise map
bae3766b
Improve simp-lemmas, add docstrings
d4e6642f
Rename circ to comp in lemma names
324f3721
Merge branch 'master' into fraction-ring-map
fa571cf2
Login to write a write a comment.
Login via GitHub