mathlib3

5d59e8bd - feat(category_theory): finite products give a monoidal structure (#1340)

feat(category_theory): finite products give a monoidal structure (#1340) * providing minimal API for limits of special shapes * apis for special shapes * start * fintype instances * copy-paste from monoidal-categories-reboot * associators, unitors, braidings for binary product * minor * minor * map * minor * instances * blah * chore(category_theory/monoidal): monoidal_category doesn't extend category * minor * minor * assoc lemma * coprod * done? * fix import * names * cleanup * fix reassoc * comments * comments