Mathlib v3 is deprecated. Go to Mathlib v4

Theorem category_theory.preadditive.is_coseparating_iff

Modification history

2022-02-21 15:30

src/category_theory/preadditive/generator.lean

feat(category_theory/preadditive): separators in preadditive categories (#11884)

Added category_theory.preadditive.is_coseparating_iff View on Github →