Ssreflect Users Discussion List

[Cyril <>]

In your case you must decide whether there exists k
such that d^k * (d^m y - d^n x) = 0, is your ring so specific that you can ?
--
Cyril

On 09/06/2017 17:01, Bas Spitters wrote:
> Yes, that was what I was thinking about.
> In our case, we only need decidable quotients.
>
> On Fri, Jun 9, 2017 at 4:57 PM, Cyril 
> <>
>  wrote:
> > 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