Ssreflect Users Discussion List

[Bas Spitters <>]

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
>>>
>
>