Ssreflect Users Discussion List

[Cyril <>]

Dear Bas and Assia,
I did consider localization when I was building the field of fractions, 
however, since S⁻¹R does not have decidable equality
(s⁻¹x = t⁻¹y iff ∃u∈S, u(sy-tx) = 0)
it does not fit the current algebraic hierarchy of math-comp.
Best,
--
Cyril

On 09/06/2017 16:39, Assia Mahboubi wrote:
> 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