mathlib3
2ec396a7 - chore(data/dfinsupp): add `dfinsupp.prod_comm` (#5817)

Commit

4 years ago

chore(data/dfinsupp): add `dfinsupp.prod_comm` (#5817) This is the same lemma as `finsupp.prod_comm` but for dfinsupp

Author

eric-wieser

Parents