Commit 2024-06-10 10:51 bdf87dca

View on Github →

refactor(Topology/Category): derive Preregular instances for Profinite and Stonean from the one on CompHaus (#12966)

Estimated changes

Modified Mathlib/Condensed/Equivalence.lean

Modified Mathlib/Topology/Category/Profinite/EffectiveEpi.lean

Modified Mathlib/Topology/Category/Stonean/EffectiveEpi.lean

deleted theorem CategoryTheory.EffectiveEpiFamily.toCompHaus