Def LightProfinite.finiteCoproduct.ι

Modification history

2024-07-31 16:34

Mathlib/Topology/Category/LightProfinite/Limits.lean

refactor(Topology/Category): use `CompHausLike` API for limits in `LightProfinite` (#15362)

Deleted LightProfinite.finiteCoproduct.ι View on Github →

2024-05-07 21:46

Mathlib/Topology/Category/LightProfinite/Limits.lean

feat(LightProfinite): (co)limits (#9513) …

Added LightProfinite.finiteCoproduct.ι View on Github →