Def CategoryTheory.Over.ConstructProducts.conesEquivFunctor

Modification history

2023-05-17 23:10

Mathlib/CategoryTheory/Limits/Constructions/Over/Products.lean

feat: port CategoryTheory.Limits.Constructions.Over.Products (#4046)

Added CategoryTheory.Over.ConstructProducts.conesEquivFunctor View on Github →