Riccardo Brasca (Nov 24 2020 at 16:38):
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
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
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
If someone wants so shed some light on what is needed to do for this kind of work any advice is very welcome!
Last updated: May 11 2021 at 17:39 UTC