Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-28 16:25 179d4d08

View on Github →

refactor(*): unify group/monoid_action, make semimodule extend action (#850)

  • refactor(*): unify group/monoid_action, use standard names, make semimodule extend action
  • Rename action to mul_action
  • Generalize lemmas. Also, add class for multiplicative action on additive structure
  • Add pi-instances
  • Dirty hacky fix
  • Remove #print and set_option pp.all
  • clean up proof, avoid diamonds
  • Fix some build issues
  • Fix build
  • Rename mul_action_add to distrib_mul_action
  • Bump up the type class search depth in some places

Estimated changes

deleted theorem mul_smul
deleted theorem one_smul
deleted theorem smul_add
deleted theorem smul_zero