Theorem CategoryTheory.IsCoseparating.of_equivalence

Modification history

2025-10-27 15:31

Mathlib/CategoryTheory/Generator/Basic.lean

refactor(CategoryTheory/Generator): use ObjectProperty instead of Set (#30269) …

Deleted CategoryTheory.IsCoseparating.of_equivalence View on Github →

2024-12-16 16:45

Mathlib/CategoryTheory/Generator.lean

feat(CategoryTheory/Abelian/GrothendieckAxioms): introduce Grothendieck categories (#18510) …

Added CategoryTheory.IsCoseparating.of_equivalence View on Github →