Theorem CategoryTheory.Limits.BinaryFan.op_mk

Modification history

2026-08-20 12:19

Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean

refactor(CategoryTheory/Limits/Shapes): split up BinaryProducts.lean (#42917) …

Modified CategoryTheory.Limits.BinaryFan.op_mk View on Github →

2025-04-01 16:59

Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean

feat(CategoryTheory/Limits): `op` for `Binary(Co)Fan` (#23537) …

Added CategoryTheory.Limits.BinaryFan.op_mk View on Github →