ReidemeisterSchreier.Profinite

2 sections | 15 files | 251 declarations

This module formalizes the profinite Reidemeister--Schreier theorem.

OpenSubgroups

This module develops Reidemeister--Schreier rewriting, Schreier generators, finite quotient transversals, and presentation transformations.

1 files | 50 declarations | 38 Theorem | 12 Definition

This module develops Reidemeister--Schreier rewriting, Schreier generators, finite quotient transversals, and presentation transformations.