mathlib3
666035fa - fix(algebra/big_operators/basic): add docstrings for `sum_bij` and `sum_bij'` (#5497)

Commit
5 years ago
fix(algebra/big_operators/basic): add docstrings for `sum_bij` and `sum_bij'` (#5497) They don't seem to be there.
Author
Parents
Loading