Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-01-26 13:49 ab155ef9

View on Github →

refactor(*): refactor sum_smul/smul_sum (#1910)

  • refactor(*): refactor sum_smul/smul_sum API changes:
  • Define both versions for list, multiset, and finset`;
  • new finset.smul_sum is the old finset.smul_sum or `root.sum_smul.symm``
  • new finset.sum_smul is the old finset.smul_sum'
  • new smul_smul doesn't need a Type argument
  • some lemmas are generalized to a semimodule or a distrib_mul_action
  • Fix compile

Estimated changes

modified theorem finset.sum_smul
added theorem list.sum_smul
added theorem multiset.sum_smul
added theorem nat.smul_def
deleted theorem smul_smul
added theorem finset.smul_sum
added theorem list.smul_sum
added theorem multiset.smul_sum
added theorem smul_smul
deleted theorem finset.smul_sum'
deleted theorem finset.smul_sum