The Fundamental Theorem of Algebra states that every polynomial over the complex numbers has a root. In Nijmegen we have formalised a constructive proof of this theorem in Coq. In this project, we wanted to also set up a library of results (about reals and complex numbers and polynomials) that could be re-used, by us and by others. We have therefore defined an algebraic hierarchy of monoids, groups, rings and so forth that allows to prove generic results and use them for concrete instantiations.
In the talk I will briefly outline the FTA project. The main part will consist of an outline of the algebraic hierarchy and its use. This part will contain an explanation of the basic features of Coq.
Reference: H. Geuvers, R. Pollack, F. Wiedijk & J. Zwanenburg, "The algebraic hierarchy of the FTA project." In: Calculemus 2001 Proceedings, Siena, Italy, 13-27, 2001. http://www.cs.kun.nl/~freek/pubs/alghier.ps.gz.