An Example of a Cofinitary Group in Isabelle/HOL

Bart Kastermans 🌐

August 4, 2009

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

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

Cite

× 
@article{CofGroups-AFP,
  author  = {Bart Kastermans},
  title   = {An Example of a Cofinitary Group in Isabelle/HOL},
  journal = {Archive of Formal Proofs},
  month   = {August},
  year    = {2009},
  note    = {\url{https://isa-afp.org/entries/CofGroups.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: