Commit 2023-10-09 12:27 159651e0

View on Github →

feat: effective epi iff surjective in CompHaus/Profinite/Stonean (#7421)

depends on: #7420

Estimated changes

Modified Mathlib/CategoryTheory/Sites/EffectiveEpimorphic.lean

added theorem CategoryTheory.effectiveEpi_iff_epi

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

added theorem CompHaus.effectiveEpi_iff_surjective

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

added theorem Profinite.effectiveEpi_iff_surjective

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

added theorem Stonean.effectiveEpi_iff_surjective