The Cartan Fixed Point Theorems Lawrence PaulsonThe 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".
Description: S/MIME Cryptographic Signature