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.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License