Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-20 13:22 b3538bfa

View on Github →

feat(topology/algebra/infinite_sum): add has_sum.smul_const etc (#10393) Rename old *.smul to *.const_smul.

Estimated changes

added theorem has_sum.const_smul
deleted theorem has_sum.smul
added theorem has_sum.smul_const
added theorem summable.const_smul
deleted theorem summable.smul
added theorem summable.smul_const
added theorem tsum_const_smul
deleted theorem tsum_smul
added theorem tsum_smul_const