Ssreflect Users Discussion List

[Bas Spitters <>]

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