Yamaguchi Lean 4 Library
Homepage
Source: ProCGroups.Order
ProCGroups
/
Order
/
Source
Source: ProCGroups.Order
1
import
ProCGroups.Order.Basic
2
3
/-!
4
# Order-theoretic constructions
5
6
This aggregate module exposes the lattice operations and finite-index estimates for closed
7
subgroups used throughout the profinite-group development.
8
-/