mathlib

da164c6b - feat (category_theory/karoubi_karoubi) : idempotence of karoubi (#11931)

feat (category_theory/karoubi_karoubi) : idempotence of karoubi (#11931) In this file, we construct the equivalence of categories `karoubi_karoubi.equivalence C : karoubi C ≌ karoubi (karoubi C)` for any category `C`. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>