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>

Author: 101damnations