The Cartan Fixed Point Theorems (Q7361783)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Cartan_FP
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | The Cartan Fixed Point Theorems |
AFP entry Cartan_FP |
Statements
8 March 2016
0 references
Lawrence C. Paulson
0 references
The Cartan Fixed Point Theorems (English)
0 references
The Cartan fixed point theorems concern the group of holomorphic automorphisms on a connected open set of C n . 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".
0 references
