Def CategoryTheory.Quotient.preadditive

Modification history

2024-07-28 23:33

Mathlib/CategoryTheory/Quotient/Preadditive.lean

chore: robustifying for debug.byAsSorry (part 13) (#15197)

Modified CategoryTheory.Quotient.preadditive View on Github →

2023-09-15 10:01

Mathlib/CategoryTheory/Quotient/Preadditive.lean

feat: the quotient category is preadditive (#7049) …

Added CategoryTheory.Quotient.preadditive View on Github →