basic): add lemma `finset.prod_dvd_prod` (#11521)

Commit

3 years ago

feat(algebra/big_operators/basic): add lemma `finset.prod_dvd_prod` (#11521) For any `S : finset α`, if `∀ a ∈ S, g1 a ∣ g2 a` then `S.prod g1 ∣ S.prod g2`.

Author

stuart-presnell

Parents

4f5d6acf

mathlib 88479be0 - feat(algebra/big_operators/basic): add lemma `finset.prod_dvd_prod` (#11521)

mathlib
88479be0 - feat(algebra/big_operators/basic): add lemma `finset.prod_dvd_prod` (#11521)