Yamaguchi Lean 4 Library
Homepage
Source: ProCGroups.ProC.GroupPredicates
ProCGroups
/
ProC
/
GroupPredicates
/
Source
Source: ProCGroups.ProC.GroupPredicates
1
import
ProCGroups.ProC.GroupPredicates.Abelian
2
3
/-!
4
# Group predicates for pro-\(C\) groups
5
6
Criteria that transfer properties of the finite quotients in an open-normal basis to the
7
underlying profinite group.
8
-/