Commit 2017-12-05 14:15 90ed0ab1

View on Github →

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

Estimated changes

Modified algebra/module.lean

added theorem add_smul

added theorem is_submodule.add_val

added theorem is_submodule.neg

added theorem is_submodule.neg_val

added theorem is_submodule.smul_val

added theorem is_submodule.sub

added theorem is_submodule.zero_val

added theorem smul_add

deleted theorem smul_left_distrib

deleted theorem smul_right_distrib

added theorem smul_sub

deleted theorem smul_sub_left_distrib

added theorem sub_smul

deleted theorem sub_smul_right_distrib

deleted theorem submodule.add_val

deleted theorem submodule.neg

deleted theorem submodule.neg_val

deleted theorem submodule.smul_val

deleted theorem submodule.sub

deleted theorem submodule.zero_val