Email Gateway (Aug 22 2022 at 12:54): 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: Nov 21 2024 at 12:39 UTC