Commit 2025-04-01 16:59 388a6d19

View on Github →

feat(CategoryTheory/Limits): op for Binary(Co)Fan (#23537) From Toric

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean

added theorem CategoryTheory.Limits.BinaryCofan.op_mk

added theorem CategoryTheory.Limits.BinaryCofan.unop_mk

added theorem CategoryTheory.Limits.BinaryFan.op_mk

added theorem CategoryTheory.Limits.BinaryFan.unop_mk