feat(Algebra/Order/BigOperators): add Finset.prod_le_prod_of_injOn (#41598)
Finset.prod_le_prod_of_injOn