Yamaguchi Lean 4 Library
Homepage
Source: ProCGroups.ProC.Category
ProCGroups
/
ProC
/
Category
/
Source
Source: ProCGroups.ProC.Category
1
import
ProCGroups.ProC.Category.Basic
2
import
ProCGroups.ProC.Category.Pullbacks
3
import
ProCGroups.ProC.Category.Pushouts
4
5
/-!
6
# Pro C Groups / pro-C / Category
7
8
This umbrella module exports the bundled category of pro-`C` groups together
9
with its pullback and pushout comparison APIs.
10
-/