basic): `finset.sum` under `mod` (#18364)

Commit

2 years ago

feat(algebra/big_operators/basic): `finset.sum` under `mod` (#18364) and `∏ a in s, f a = b ^ s.card` if `f a = b` for all `a`

Author

YaelDillies

Parents