mathlib3
228d5bad - feat(algebra/big_operators): sum_eq_zero_iff_of_nonpos (#1424)

Commit

6 years ago

feat(algebra/big_operators): sum_eq_zero_iff_of_nonpos (#1424) * feat(algebra/big_operators): sum_eq_zero_iff_of_nonpos * more order_dual instances

References

Author

ChrisHughes24

Committer

mergify[bot]

Parents