feat(algebra/big_operators/finprod): finprod_eq_one_of_forall_eq_one (#11335)
finprod_eq_one_of_forall_eq_one