Improve `ring_theory/localization`

Stream: maths

[Riccardo Brasca]

Following a suggestion of @Johan Commelin (that is busy with other stuff) in #maths > Minimal polynomial over ℚ vs over ℤ I would like to improve ring_theory/localization. The problem is that is seems impossible (to me at least) or in any case very complicated to use results like gcd_domain_eq_field_fractions, where we have a monoid R with field of fractions K and an K-algebra L, in concrete situation, for example when R = ℤ. More precisely, I am not able to prove gcd_domain_eq_field_fractions in the case the GCD monoid is ℤ using gcd_domain_eq_field_fractions (of course redoing the proof in this case is easy).

I can do the "unskilled work", but I need some guidance. For example, Johan suggests that

is_localization (R A : Type*) [comm_ring R] [comm_ring A] [algebra R A] : Prop :=

should be a proposition. Should it be a structure? A class?

If someone wants so shed some light on what is needed to do for this kind of work any advice is very welcome!