mathlib3

e75326d4 - feat(category/idempotents): extension of functors to the idempotent completion (#15746)

feat(category/idempotents): extension of functors to the idempotent completion (#15746) This PR show that functors `C ⥤ karoubi D` can be canonically extended to functors `karoubi C ⥤ karoubi D`.