# The Cartan Fixed Point Theorems

 Title: The Cartan Fixed Point Theorems Author: Lawrence C. Paulson Submission date: 2016-03-08 Abstract: 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". BibTeX: ```@article{Cartan_FP-AFP, author = {Lawrence C. Paulson}, title = {The Cartan Fixed Point Theorems}, journal = {Archive of Formal Proofs}, month = mar, year = 2016, note = {\url{http://isa-afp.org/entries/Cartan_FP.html}, Formal proof development}, ISSN = {2150-914x}, }``` License: BSD License