Def CategoryTheory.Over.ConstructProducts.conesEquivUnitIso

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.conesEquivUnitIso View on Github →