ssreflect - [ssreflect] Localization of a ring

Subject: Ssreflect Users Discussion List

List archive

[ssreflect] Localization of a ring

From: Bas Spitters <>
To: Ssreflect-mailinglist <>
Subject: [ssreflect] Localization of a ring
Date: Fri, 9 Jun 2017 14:08:24 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None ; spf=Pass ; spf=None
Ironport-phdr: 9a23:/IfrRRZKPHptDtmYul2LAi//LSx+4OfEezUN459isYplN5qZr86zbnLW6fgltlLVR4KTs6sC0LuJ9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQtFiT6/bL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjm58axlVAHnhzsGNz4h8WHYlMpwjL5AoBm8oxBz2pPYbJ2JOPZ7eK7WYNEUSndbXstJVyJPDICyYZYRAeUdJutYs5XxqkESoReiGQWhBuXiwSJIiH/s2q061vwsHBzc0ww7AtkArWzUrNTpNKcOT++11rLIxijEYvxNwzvy8pLEcx47rfGXRbJwcNbRyVUxGAPflVWdsoPlPzaP2eQMt2iX9fZvVeWqi2M+rQx6vzahxsApiobTh4IVzEjJ9Ct4wIY2JN24UFB0bsOlEJRKrS2aMJF2QswkTmp1uyg60qULtYCncCUO0pgqxB7SZ+aZf4SV7B/vTumcLDh+iXl4YrywnQyy/lKlyuDkVsm7zlJKri1dn9nJrH8N1hjT5tGZSvt+4kutwDiP2g/c5+1eLkA0kq3bK5ElwrEujJYcrUPDHirulEX3iq+ZaFkk9/C25+j7ZrjqvJyROo9uhg3gL6gjlNazDOs3PwQWWmiU4+W81Lnt/U3jR7VKi+U7nbLDvJ/AP8gaqLS1AxRN0oYi9xa/Eymp0M4DnXQcI1JFfQiIj4ntO13UPP/4CvK/j0y2kDh33/DGIqHhApLVI3jYi7fhZ6hy60BYyAUt0d9f+4lZCqoBIfL2Qk/+rsbUDh4/MwyuwuboEs9x1o0EWTHHPqjMC7jIvFGM6+kzZuyFZYsUvjn5KuM5r6r1lmU0l1sQdrWB2IANLXG+BPVvZUSfe3vlxNkbRzQkpA07GcbjkxW5ST9Pe3uoROpo7HcyTp3gFp/CWpygmqep0yKyH5kQbWdDXAPfWUz0fpmJDq9fIBmZJdVsx3ldDeCs

Does ssr have a theory of localization of a ring ?
https://en.wikipedia.org/wiki/Localization_of_a_ring

I think we only need the case where the denominators are generated by
one element.

I've found the formalization of the field of fractions, so if nothing
else, we'll probably try to adapt that.

Thanks,

Bas

[ssreflect] Localization of a ring, Bas Spitters, 06/09/2017
- Re: [ssreflect] Localization of a ring, Assia Mahboubi, 06/09/2017
  - Re: [ssreflect] Localization of a ring, Bas Spitters, 06/09/2017
    - Re: [ssreflect] Localization of a ring, Assia Mahboubi, 06/09/2017
      - Re: [ssreflect] Localization of a ring, Cyril, 06/09/2017
        
        Re: [ssreflect] Localization of a ring, Bas Spitters, 06/09/2017
        
        Re: [ssreflect] Localization of a ring, Cyril, 06/09/2017
        
        Re: [ssreflect] Localization of a ring, Bas Spitters, 06/09/2017
        Re: [ssreflect] Localization of a ring, Cyril, 06/09/2017

List archive

[ssreflect] Localization of a ring