ReidemeisterSchreier

7 sections | 59 files | 1078 declarations

This module formalizes the Reidemeister--Schreier theorem.

Discrete

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

This module formalizes free-group tools used in Reidemeister--Schreier rewriting.

1 files | 4 declarations | 1 Theorem | 2 Lemma | 1 Definition

This module formalizes the groupoid version of the spanning-tree basis construction.

This module formalizes the profinite Reidemeister--Schreier theorem.

1 files | 2 declarations | 2 Definition

This module formalizes the quiver and arborescence tools used by the groupoid construction.

1 files | 9 declarations | 5 Theorem | 3 Definition | 1 Abbreviation

This module formalizes right quotients and transversals for subgroup rewriting.

1 files | 7 declarations | 6 Theorem | 1 Definition

This module formalizes Schreier generators and rewriting.