Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-12-20 20:34 883d974b

View on Github →

feat(algebra/module): sum_smul' (for semimodules) (#1752)

  • feat(algebra/module): sum_smul' (for semimodules)
  • adding docstring
  • use classical tactic
  • moving ' name to the weaker theorem

Estimated changes