Mathlib v3 is deprecated. Go to Mathlib v4

Theorem smul_left_distrib

Modification history

2017-12-05 14:15
algebra/module.lean
refactor(algebra/module): rename submodule -> is_submodule, smul_left_distrib -> smul_add, smul_right_distrib -> add_smul, smul_sub_left_distrib -> smul_sub, sub_smul_right_distrib -> sub_smul
Deleted smul_left_distribView on Github →
2017-11-06 03:28
algebra/module.lean
refactor(algebra/module): clean up PR commit
Modified smul_left_distribView 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 smul_left_distribView on Github →
2017-08-26 15:40
algebra/module.lean
feat(algebra): porting modules from lean2
Added smul_left_distribView on Github →