Ssreflect Users Discussion List

[Assia Mahboubi <>]

Hi Bas,

Le 09/06/2017 à 14:08, Bas Spitters a écrit :
> Does ssr have a theory of localization of a ring ?
> https://en.wikipedia.org/wiki/Localization_of_a_ring

As such, not in math-comp I would say.

> I think we only need the case where the denominators are generated by
> one element.

Could you provide some more context about what you need?

Best,

assia

> I've found the formalization of the field of fractions, so if nothing
> else, we'll probably try to adapt that.
> 
> Thanks,
> 
> Bas
>