Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-10 23:19 c2958736

View on Github →

feat(algebra/module/basic): {nat,int}_smul_apply (#5308)

Estimated changes

Modified src/algebra/module/basic.lean

added theorem add_monoid_hom.int_smul_apply

modified theorem add_monoid_hom.map_int_cast_smul

modified theorem add_monoid_hom.map_int_module_smul

modified theorem add_monoid_hom.map_nat_cast_smul

modified theorem add_monoid_hom.map_rat_cast_smul

modified theorem add_monoid_hom.map_rat_module_smul

added theorem add_monoid_hom.nat_smul_apply