mathlib

09ea7fb0 - feat(data/finset/noncomm_prod): finite pi lemmas (#12291)

feat(data/finset/noncomm_prod): finite pi lemmas (#12291) including a few helpers Co-authored-by: Junyan Xu <junyanxumath@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>