Commit 2024-08-06 05:02 123eb213

View on Github →

feat(CategoryTheory): opposite functors preserving finite products (#15518) If F preserves finite coproducts, then F.op preserves finite products, and the seven other variants for leftOp, unop etc. Also remove some lean3-isms from docstrings

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Preserves/Opposites.lean

added def CategoryTheory.Limits.preservesFiniteCoproductsLeftOp

added def CategoryTheory.Limits.preservesFiniteCoproductsOp

added def CategoryTheory.Limits.preservesFiniteCoproductsRightOp

added def CategoryTheory.Limits.preservesFiniteCoproductsUnop

added def CategoryTheory.Limits.preservesFiniteProductsLeftOp

added def CategoryTheory.Limits.preservesFiniteProductsOp

added def CategoryTheory.Limits.preservesFiniteProductsRightOp

added def CategoryTheory.Limits.preservesFiniteProductsUnop