mathlib3

80ad9edc - refactor(ring_theory/localization): characterise ring localizations up to isomorphism (#2714)

refactor(ring_theory/localization): characterise ring localizations up to isomorphism (#2714) Beginnings of ```ring_theory/localization``` refactor from #2675. It's a bit sad that using the characteristic predicate means Lean can't infer the R-algebra structure of the localization. I've tried to get round this, but I'm not using •, and I've duplicated some fairly random lemmas about modules & algebras to take ```f``` as an explicit argument - mostly just what I needed to make ```fractional_ideal``` work. Should I duplicate more? My comments in the ```fractional_ideal``` docs about 'preserving definitional equalities' wrt getting an R-module structure from an R-algebra structure: do they make sense? I had some errors about definitional equality of instances which I *think* I fixed after making sure the R-module structure always came from the R-algebra structure, as well as doing a few other things. I never chased up exactly what the errors were or how they went away, so I'm just guessing at my explanation. Things I've got left to PR to ```ring_theory/localization``` after this: - ```away``` (localization at submonoid generated by one element) - localization as a quotient type & proof it satisfies the char pred - localization at the complement of a prime ideal and the fact this is a local ring - more lemmas about fields of fractions - the order embedding for ideals of the localization vs. ideals of the original ring Co-authored-by: Amelia Livingston <40745104+101damnations@users.noreply.github.com>