Commit 2023-04-06 10:44 0ad947c7

View on Github →

feat: port CategoryTheory.Idempotents.Basic (#3290)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Idempotents/Basic.lean

added theorem CategoryTheory.Idempotents.Equivalence.isIdempotentComplete

added theorem CategoryTheory.Idempotents.idem_of_id_sub_idem

added theorem CategoryTheory.Idempotents.isIdempotentComplete_iff_hasEqualizer_of_id_and_idempotent

added theorem CategoryTheory.Idempotents.isIdempotentComplete_iff_idempotents_have_kernels

added theorem CategoryTheory.Idempotents.isIdempotentComplete_iff_of_equivalence

added theorem CategoryTheory.Idempotents.isIdempotentComplete_iff_opposite

added theorem CategoryTheory.Idempotents.isIdempotentComplete_of_isIdempotentComplete_opposite

added theorem CategoryTheory.Idempotents.split_iff_of_iso

added theorem CategoryTheory.Idempotents.split_imp_of_iso