Ssreflect Users Discussion List

[Assia Mahboubi <>]

Hi Bas,

Le 09/06/2017 à 16:31, Bas Spitters a écrit :
> Hi Assia,
> 
> Consider a ring R and d: R.
> We'd need the localization R[1/d] with respect to the multiplicative
> set S={1, d, d^2, ...}, the ring of fractions.

This looks indeed like the definition of the localization, in this special 
case.
But I was wondering (out of sheer curiosity) about the more general context in
which you need this construction.

assia

> If it is not there, we'll probably just adapt if from the field of 
> fractions.
> 
> Best,
> 
> Bas
>