Non-constructive complex analysis in Coq

DOI10.4230/LIPICS.TYPES.2011.1MaRDI QIDQ2957693zbMATH OpenOpenAlexFDO

Authors Aloïs Brunel

Publication date 27 January 2017

Full work available at URL https://drops.dagstuhl.de/opus/volltexte/2013/3896/pdf/2.pdf

zbMATH Keywords

complex analysisCoqwinding number

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Software, source code, etc. for problems pertaining to functions of a complex variable (30-04) Software, source code, etc. for problems pertaining to algebraic topology (55-04)

Recommendations

• scientific article; zbMATH DE number 2085169
• The fundamental theorem of algebra: a constructive development without choice.
• A formal proof of Cauchy's residue theorem
• A Nonstandard Proof of the Fundamental Theorem of Algebra
• A constructive version of Sperner's lemma and Brouwer's fixed point theorem

Cited in

(2)

• Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL
• Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives

Describes a project that uses

Uses Software

• Coqtail
• Coq

This page was built for publication: Non-constructive complex analysis in Coq

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2957693)