coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Monoid and Group definition missing in setoid_ring directory

From: mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Monoid and Group definition missing in setoid_ring directory
Date: Tue, 10 Dec 2019 23:12:05 +1100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mukeshtiwari.iiitm AT gmail.com; spf=Pass smtp.mailfrom=mukeshtiwari.iiitm AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm1-f50.google.com
Ironport-phdr: 9a23:g1pFch3Em/wxyo/esmDT+DRfVm0co7zxezQtwd8Zse0eKPad9pjvdHbS+e9qxAeQG9mCsLQd2rGd6P2ocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmTSwbalvIBiyowjduccbjIt/Iast1xXFpWdFdf5Lzm1yP1KTmBj85sa0/JF99ilbpuws+c1dX6jkZqo0VbNXAigoPGAz/83rqALMTRCT6XsGU2UZiQRHDg7Y5xznRJjxsy/6tu1g2CmGOMD9UL45VSi+46ptVRTljjoMOTwk/2HNksF/g6JVrhyiqRJi3YDbfJqYNOZicq7HYd8WWXZNU8RXWidcAo28dYwPD+8ZMOZdson9pEUBrQC+BQKxGOPvyzFJiWXs3a07zu8sFgTG3BEjH90Qq3TUrMn1NKYcUO+v1qnIzC/Pb/JX2Tf89IjIdwssof6JXb1qcMrRzVMjGB/CjlWVsIHoOS6e2OoKs2ie9eVgVOSvhnYoqwFwvjivxtoshZLTio0JzVDE8CN0y5s2K92gUEN3f8KoHZ9KuyyZN4Z6WN4uT39rtSogyrAKpZi2dzUQxps93R7QcfmHfpCI4h39UOaRJi91hHd/d7K+gxa+6EahyujhWsWt3lZHrjZJnsPDtnAK0BzT5cyHReVn8ki93jaP0hjf6uBCIU8qiarWM4AtzqI0m5YJsknOHjX6lFjogKKVbEkp+vSk5/ziYrr8p5+cM4F0ihv5MqQrgsG/BPk4MgsQUGiA+eS8yLzj/EPjT7VQj/06iKjZsJHbJcQHo660GABV0oM55Ba+CzeqysgXnX4CLF5dYhKIk5DpO03SIPD/Ffqwn1OskC5yy//aOr3hH47CI2PYkLbheLZ981RTxBAyzdBZ/ZJUC6sOLOj9Wk/r55TkCUoyNBXxyOL6Av180JkfUCSBGPy3KqTX5FqV5e80I6GQZZAcoje1f/045PP1jWM4hlYHfO+o3JoLbVi3G/1nJwOSZn+60YRJKnsDogdrFL+is1aFSzMGPy/uDZJ53SkyDcedNamGXpqk2eXT0yKyH5kQbWdDWAjVTCXYMr6cUvJJUxq8Z89sljteCOqkQo4lkA6r7Ur0luIhIe3T9SkV85nk0YotvryBpVQJ7TVxSv+l/SSIRmBwkHkPQmZvjq96qE15jFyE1Pohjg==

Hi Everyone,

I was browsing the source code [1]. In this directory, we have the
definition of Ring [2] and Field [3], and lemmas about them, but I am
wondering why don't we have Monoid and Group?

Best,
Mukesh

[1]
https://github.com/coq/coq/tree/d886dff0857702fc4524779980ee6b7e9688c1d4/plugins/setoid_ring
[2]
https://github.com/coq/coq/blob/d886dff0857702fc4524779980ee6b7e9688c1d4/plugins/setoid_ring/Ring_theory.v
[3]
https://github.com/coq/coq/blob/d886dff0857702fc4524779980ee6b7e9688c1d4/plugins/setoid_ring/Field_theory.v

[Coq-Club] Monoid and Group definition missing in setoid_ring directory, mukesh tiwari, 12/10/2019