- There is a paper in english describing this work, here is the final version.
The code for the running example about integers can be found in quotint.v.
- Here are the sources as a tarball : quotients.tgz.
This is a partial snapshot of the Mathematical Components project, so it contains lots of files I did not write. The purpose of this snapshot is to highlight my personal work on quotients, through several files of mine:
- generic_quotient.v that contains my library on quotienting.
- ring_quotient.v which contains its applications to quotients of a ring by an ideal
- multinom.v and fraction.v which are direct applications of quotients (but not used in the proof of Feit-Thompson theorem)
- realalg.v which builds real algebaic numbers for the proof of Feit-Thompson theorem
I did not include the applications of quotients that I did not write myself.
(Those archive are self-contained and are based on previous versions of quotient types.)
- the algebraic closure of a countable field and Galois theory, which can be found in the Feit-Thompson proof
- elliptic curves
This page was last updated at
2014-12-01 03:52:16 +0100
