mathlib3
feat(topology/algebra/infinite_sum) : define infinite products
#19219
Open
Open