# 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{https://isa-afp.org/entries/Cartan_FP.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.