ReidemeisterSchreier.Discrete

3 sections | 35 files | 766 declarations

This module formalizes the classical discrete Reidemeister--Schreier theorem.

OpenSubgroups

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

12 files | 304 declarations | 150 Theorem | 149 Definition | 5 Structure

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

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