Commit 2025-01-26 20:04 0b484e16

View on Github →

chore: deduplicate proof that coproduct of separating set is separator (#21081)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Generator/Basic.lean

added theorem CategoryTheory.IsSeparating.isSeparator_coproduct

added theorem CategoryTheory.isSeparator_of_isColimit_cofan

Deleted Mathlib/CategoryTheory/Generator/Coproduct.lean

deleted theorem CategoryTheory.IsSeparating.isSeparator_coproduct

deleted theorem CategoryTheory.IsSeparating.isSeparator_of_isColimit_cofan

Modified Mathlib/CategoryTheory/Generator/Presheaf.lean