Pushouts.lean
Nyll.ProCGroups.ProC.Category.Pushouts
0 declarations indexed from sourceView source ↗
Module documentation
Pro C Groups / pro-C / Category / Pushouts
Pushout universal properties in ProCGrp C use mathlib's CategoryTheory.IsPushout predicate and its standard desc, factorization, extensionality, and comparison-isomorphism API. This module remains as the stable import boundary for those definitions.
Imports2
- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
- Nyll.ProCGroups.ProC.Category.Basic
Imported by1
This module has no indexed declarations. Its imports and full source are available here.