Non-constructive complex analysis in Coq

DOI10.4230/LIPICS.TYPES.2011.1zbMATH Open1354.68231OpenAlexW2790102975MaRDI QIDQ2957693FDOQ2957693

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

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

zbMATH Keywords

Coqwinding numbercomplex analysis

Mathematics Subject Classification ID

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

Cited In (2)

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

Uses Software

• Coq
• Coqtail

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)