mathlib3

f8db86a2 - feat(category_theory/limits): finite products from binary products (#5516)

feat(category_theory/limits): finite products from binary products (#5516) Adds constructions for finite products from binary products and terminal object, and a preserves version