Commit 2022-01-25 03:33 88479be0
View on Github →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.
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.