- Here is the article describing this work, slightly improved from the submitted version.
- The code that is not yet in the published ssreflect archive can be found hereafter :
- polydiv.v that adds properties about polynomials
- closed_field.v that defines the projection operator and states its proof (as said in the above article)
- Finally, here is a partial (restricted to our purpose) html documentation of the archive plus the above files, stating only comments, definitions and lemmas (removing the proof scripts for readability)
This page was last updated at
2014-12-01 03:52:16 +0100
