Def CategoryTheory.Limits.Over.coprodObj

Modification history

2026-10-08 18:10

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

chore(CategoryTheory/Limits/Shapes/BinaryProducts): use `to_dual` (#43571) …

Added CategoryTheory.Limits.Over.coprodObj View on Github →