Mathlib v3 is deprecated. Go to Mathlib v4

Theorem mul_smul

Modification history

2020-10-31 17:41
src/group_theory/group_action.lean
chore(group_theory/group_action): introduce `smul_comm_class` (#4770)
Deleted mul_smulView on Github →
2019-03-28 16:25
src/algebra/module.lean
refactor(*): unify group/monoid_action, make semimodule extend action (#850) …
Modified mul_smulView on Github →
2018-11-05 10:47
algebra/module.lean
feat(linear_algebra,ring_theory): refactoring modules (#456) …
Modified mul_smulView on Github →
2018-09-10 13:57
algebra/module.lean
feat(algebra/module): semimodules
Modified mul_smulView on Github →
2017-11-06 03:28
algebra/module.lean
refactor(algebra/module): clean up PR commit
Modified mul_smulView on Github →
2017-08-27 12:26
algebra/module.lean
fix(.): adapt to Lean changes: type class parameters to structures are now type class parameters in the projections and constructor
Modified mul_smulView on Github →
2017-08-26 15:40
algebra/module.lean
feat(algebra): porting modules from lean2
Added mul_smulView on Github →