Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-01 14:22 a4e936ca

View on Github →

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

Estimated changes

Modified src/category_theory/idempotents/basic.lean

added theorem category_theory.idempotents.idem_of_id_sub_idem

deleted theorem category_theory.idempotents.idempotence_of_id_sub_idempotent

Modified src/category_theory/idempotents/biproducts.lean

Modified src/category_theory/idempotents/functor_categories.lean

Modified src/category_theory/idempotents/karoubi.lean

modified def category_theory.idempotents.karoubi.decomp_id_i

modified theorem category_theory.idempotents.karoubi.id_eq

modified structure category_theory.idempotents.karoubi

Modified src/category_theory/idempotents/karoubi_karoubi.lean