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

Commit
3 years ago
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`.
Author
Parents
Loading