The Cartan Fixed Point Theorems

Lawrence C. Paulson 🌐

March 8, 2016

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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".


BSD License


Session Cartan_FP