mathlib3

1142e0b7 - feat(big_operators/fin): sum over elements of vector equal to `a` equals count `a` (#15360)

feat(big_operators/fin): sum over elements of vector equal to `a` equals count `a` (#15360) The sum over `i : fin n` of 1 for vector elements equal to some `a` is just count applied to `a`. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>