An Example of a Cofinitary Group in Isabelle/HOL

Bart Kastermans 🌐

August 4, 2009

Abstract

We formalize the usual proof that the group generated by the function k -> k + 1 on the integers gives rise to a cofinitary group.

License

BSD License

Topics

Session CofGroups