Mathlib v3 is deprecated. Go to Mathlib v4

Theorem category_theory.idempotents.idem_of_id_sub_idem

Modification history

2022-03-01 14:22
src/category_theory/idempotents/basic.lean
chore(category_theory/idempotents) replaced "idempotence" by "idem" (#12362)
Added category_theory.idempotents.idem_of_id_sub_idemView on Github →