Def CategoryTheory.Idempotents.FunctorExtension₁.obj

Modification history

2023-04-06 15:15

Mathlib/CategoryTheory/Idempotents/FunctorExtension.lean

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

Added CategoryTheory.Idempotents.FunctorExtension₁.obj View on Github →