# Zulip Chat Archive

## Stream: maths

### Topic: Improve `ring_theory/localization`

#### 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 `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!

Last updated: May 11 2021 at 17:39 UTC