chore: deprecate `monoidalOfHasFiniteProducts`#30684

YaelDillies wants to merge 2 commits intoleanprover-community:masterleanprover-community/mathlib4:masterfrom

YaelDillies:deprecate_monoidal_of_has_finite_productsYaelDillies/mathlib4:deprecate_monoidal_of_has_finite_productsCopy head branch name to clipboard