Mathlib v3 is deprecated. Go to Mathlib v4

Theorem category_theory.idempotents.idempotence_of_id_sub_idempotent

Modification history

2022-03-01 14:22

src/category_theory/idempotents/basic.lean

chore(category_theory/idempotents) replaced "idempotence" by "idem" (#12362)

Deleted category_theory.idempotents.idempotence_of_id_sub_idempotent View on Github →

2022-02-09 07:16

src/category_theory/idempotents/basic.lean

feat(category_theory/pseudoabelian/basic): basic facts and contructions about pseudoabelian categories (#11817)

Added category_theory.idempotents.idempotence_of_id_sub_idempotent View on Github →