Commit 2023-04-06 16:41 b56224ca

View on Github →

feat: port CategoryTheory.Idempotents.KaroubiKaroubi (#3298)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Idempotents/KaroubiKaroubi.lean

added def CategoryTheory.Idempotents.KaroubiKaroubi.counitIso

added def CategoryTheory.Idempotents.KaroubiKaroubi.equivalence

added theorem CategoryTheory.Idempotents.KaroubiKaroubi.idem_f

added def CategoryTheory.Idempotents.KaroubiKaroubi.inverse

added theorem CategoryTheory.Idempotents.KaroubiKaroubi.p_comm_f

added def CategoryTheory.Idempotents.KaroubiKaroubi.unitIso