Mathlib v3 is deprecated. Go to Mathlib v4

Theorem sub_smul

Modification history

2020-04-13 05:19

src/algebra/module.lean

chore(algebra/module): rename type vars, minor cleanup, add module docstring (#2392) …

Modified sub_smul View on Github →

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

Added sub_smul View on Github →