Commit 2022-07-26 02:21 1142e0b7
View on Github →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.
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.