mathlib3

0e8cca36 - feat(algebra/big_operators/order): `prod_eq_prod_iff_of_le` (#11068)

feat(algebra/big_operators/order): `prod_eq_prod_iff_of_le` (#11068) If `f i ≤ g i` for all `i ∈ s`, then `∏ i in s, f i = ∏ i in s, g i` if and only if `f i = g i` for all `i ∈ s`.