Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP article: The Cartan Fixed Point Theorems


view this post on Zulip Email Gateway (Aug 22 2022 at 12:54):

From: Tobias Nipkow <nipkow@in.tum.de>
The Cartan Fixed Point Theorems
Lawrence Paulson

The Cartan fixed point theorems concern the group of holomorphic automorphisms
on a connected open set of Cn. Ciolli et al. have formalised the one-dimensional
case of these theorems in HOL Light. This entry contains their proofs, ported to
Isabelle/HOL. Thus it addresses the authors~ remark that "it would be important
to write a formal proof in a language that can be read by both humans and
machines".

http://afp.sourceforge.net/entries/Cartan_FP.shtml

Enjoy!
smime.p7s


Last updated: Mar 29 2024 at 08:18 UTC