Ssreflect Users Discussion List

[Cyril <>]

Oh, you want this for an integral domain! Ok then...
I never though of specializing localization for integral domain since 
you could build the field of fractions anyway, but since you have a use 
case...
--
Cyril

On 09/06/2017 17:11, Bas Spitters wrote:
> R is a domain with decidable equality, which should be enough.
>
> Best,
>
> Bas
>
> On Fri, Jun 9, 2017 at 5:04 PM, Cyril 
> <>
>  wrote:
> > 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