Commit 2024-11-10 14:44 b17bf258
View on Github →chore(CategoryTheory/Abelian/GrothendieckAxioms): remove unnecessary premise, clarify definition of AB4/5 (#18810)
Remove the unnecessary HasFiniteCoproducts premise from AB4.ofAB5 and clarify in the module docstring that the typeclasses AB4 and AB5 don't require Abelian.