Theorem CategoryTheory.Idempotents.functorExtension₁_comp

Modification history

2023-11-24 14:23

Mathlib/CategoryTheory/Idempotents/FunctorExtension.lean

refactor(CategoryTheory/Idempotents): replacing equalities of functors by isomorphisms (#8562) …

Deleted CategoryTheory.Idempotents.functorExtension₁_comp View on Github →

2023-04-06 15:15

Mathlib/CategoryTheory/Idempotents/FunctorExtension.lean

feat: port CategoryTheory.Idempotents.FunctorExtension (#3300)

Added CategoryTheory.Idempotents.functorExtension₁_comp View on Github →