Theorem CategoryTheory.ObjectProperty.binaryCoproductsClosure_le_iff

Modification history

2026-10-30 15:08
Mathlib/CategoryTheory/ObjectProperty/BinaryProductsClosure.lean
chore(CategoryTheory): deprecate `leftExactFunctor` (#45418) …
Modified CategoryTheory.ObjectProperty.binaryCoproductsClosure_le_iffView on Github →
2026-03-24 13:52
Mathlib/CategoryTheory/ObjectProperty/FiniteProducts.lean
feat(CategoryTheory/ObjectProperty): `binaryProductsClosure` (#37085) …
Added CategoryTheory.ObjectProperty.binaryCoproductsClosure_le_iffView on Github →