Def CategoryTheory.Idempotents.KaroubiUniversal₁.counitIso

Modification history

2023-04-06 15:15

Mathlib/CategoryTheory/Idempotents/FunctorExtension.lean

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

Added CategoryTheory.Idempotents.KaroubiUniversal₁.counitIso View on Github →