[isabelle] New AFP article: The Cartan Fixed Point Theorems

The Cartan Fixed Point Theorems
Lawrence Paulson

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



Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.