Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finset.sum_const_zero

Modification history

2021-07-05 15:47
src/algebra/big_operators/basic.lean
feat(algebra/to_additive): map pow to smul (#7888) …
Deleted finset.sum_const_zeroView on Github →
2021-06-29 21:36
src/algebra/big_operators/basic.lean
feat(algebra/to_additive): do not additivize operations on constant types (#7792) …
Modified finset.sum_const_zeroView on Github →
2020-03-03 11:51
src/algebra/big_operators.lean
feat(tactic/lint): check for redundant simp lemmas (#2066) …
Modified finset.sum_const_zeroView on Github →
2018-04-03 21:23
algebra/big_operators.lean
fix(*): update to lean …
Added finset.sum_const_zeroView on Github →