Commit 2025-02-22 10:33 5a769dba
View on Github →feat(CategoryTheory): forgetting the group structure on the codomain of left-exact functors (#21973)
This is the miracle that will allow us to discover a preadditive structure on Ind C if C is (small and) additive.