Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-21 13:41 ac3ae212

View on Github →

refactor(category_theory/limits/shapes/finite_products): review API, fix lint (#17623)

Redefine category_theory.limits.has_finite_products to use fin n instead of any finite Type.
Merge has_limits_of_shape_discrete with a more general has_fintype_products.
Do similar changes to *_coproducts.

Estimated changes

Modified src/algebra/category/Module/abelian.lean

Modified src/category_theory/closed/ideal.lean

Modified src/category_theory/extensive.lean

Modified src/category_theory/idempotents/biproducts.lean

Modified src/category_theory/limits/constructions/finite_products_of_binary_products.lean

Modified src/category_theory/limits/constructions/over/products.lean

Modified src/category_theory/limits/opposites.lean

Modified src/category_theory/limits/shapes/biproducts.lean

added theorem category_theory.limits.has_biproducts_of_shape_of_equiv

Modified src/category_theory/limits/shapes/finite_products.lean

Modified src/category_theory/preadditive/Mat.lean

Modified src/category_theory/preadditive/biproducts.lean

Modified src/representation_theory/Action.lean

Modified src/topology/sheaves/abelian.lean