The Fundamental Theorem of Algebra

Description: This library contains the constructive proof of the Fundamental Theorem of Algebra, along the lines of the proof of Kneser, which originally appeared in Kneser?? (but see also TvD?? for a presentation). We have adapted (improved and made more precise, as we would view it) the proof quite a bit; an account of the formalised mathematical proof is presented in GeuWieZwa??. This library rests on the algebraic hierarchy, which defines all the basic concepts, like the reals, the complex numbers, polynomials etc. The FTA library contains more specific operations on and properties of the reals, the complex numbers and polynomials, required for the FTA proof. Furthermore it contains the Kneser proof, devided in 4 stages.

• results about preservation of continuity through algebraic operations;
• the usual rules for derivation; - formalization of power series and Taylor series;
• several formulations of Rolle's Theorem, the Mean Law, convergence theorems and error estimates for Taylor series;
• the Key Lemma and the Main Lemma, stating results about (finite sequences of) reals, specifically needed for FTA. (These are more or less implicit in the original proof of Kneser);
• the Kneser Lemma
• FTA for regular polynomials (i.e. where we know that the leading coefficient is 1);
• FTA for arbitrary non-constant polynomials.

References:  

• For the mathematical content:
• Bishop, E., "Foundations of Constructive Analysis", McGraw-Hill Book Company, 1967
•  About the formalization itself:
• Cruz-Filipe, L., "Formalizing Real Calculus in Coq", in  Theorem Proving in Higher Order Logics , Carreño, V., Muñoz, C. and Tahar, S. (eds.), NASA Conference Proceedings, Hampton VA, 2002 (ps, pdf)

Maintainer: Freek Wiedijk

Developers: Henk Barendregt, Herman Geuvers, Randy Pollack, Jan Zwanenburg

Documentation

Download