Def CategoryTheory.Idempotents.FunctorExtension₁.map

Modification history

2023-04-06 15:15

Mathlib/CategoryTheory/Idempotents/FunctorExtension.lean

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

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