The Cartan Fixed Point Theorems

Lawrence C. Paulson 🌐

March 8, 2016

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

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".

License

BSD License

Topics

Session Cartan_FP

Cite

× 
@article{Cartan_FP-AFP,
  author  = {Lawrence C. Paulson},
  title   = {The Cartan Fixed Point Theorems},
  journal = {Archive of Formal Proofs},
  month   = {March},
  year    = {2016},
  note    = {\url{https://isa-afp.org/entries/Cartan_FP.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: