Formalization of the Lindemann-Weierstrass theorem

DOI10.1007/978-3-319-66107-0_5zbMath1483.68485OpenAlexW2748775531MaRDI QIDQ1687717

Sophie Bernard

Publication date: 4 January 2018

Full work available at URL: https://hal.inria.fr/hal-01647563/file/main.pdf

zbMATH Keywords

transcendencemultivariate polynomialsformal proofsCoqpolynomial conjugates

Mathematics Subject Classification ID

Transcendence (general theory) (11J81) Formalization of mathematics in connection with theorem provers (68V20)

Uses Software

• Coq

Cites Work

• Coquelicot: a user-friendly library of real analysis for Coq
• Formalization of Bernstein polynomials and applications to global optimization
• A Machine-Checked Proof of the Odd Order Theorem
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Formalization of the Lindemann-Weierstrass theorem