mathlib3
a58ae545 - chore(algebra/big_operators/finprod): remove outdated todo (#9900)

Commit

4 years ago

chore(algebra/big_operators/finprod): remove outdated todo (#9900)

Author

kex-y

kex-y

Parents

Loading