Yamaguchi Lean 4 Library
Homepage
Source: ProCGroups.Profinite
ProCGroups
/
Profinite
/
Source
Source: ProCGroups.Profinite
1
import
ProCGroups.Profinite.Basic
2
3
/-!
4
# Profinite groups
5
6
This aggregate module exposes separation and permanence results for profinite groups and their
7
open subgroups.
8
-/