finprod): add lemma `finprod_eq_prod_of_mul_support_to_finset_subset'` (#13801)

Commit

3 years ago

feat(algebra/big_operators/finprod): add lemma `finprod_eq_prod_of_mul_support_to_finset_subset'` (#13801) Formalized as part of the Sphere Eversion project.

Author

ocfnash

Parents

65843cdc

mathlib af11e154 - feat(algebra/big_operators/finprod): add lemma `finprod_eq_prod_of_mul_support_to_finset_subset'` (#13801)

mathlib
af11e154 - feat(algebra/big_operators/finprod): add lemma `finprod_eq_prod_of_mul_support_to_finset_subset'` (#13801)