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".
  author  = {Lawrence C. Paulson},
  title   = {The Cartan Fixed Point Theorems},
  journal = {Archive of Formal Proofs},
  month   = mar,
  year    = 2016,
  note    = {\url{},
            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.