Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-23 01:05 6aa5572e

View on Github →

feat(algebra/module): f : E →+ F is ℚ-linear (#2215)

feat(algebra/module): f : E →+ F is ℚ-linear Also cleanup similar lemmas about ℕ and ℤ.
Fix a typo

Estimated changes

Modified src/algebra/direct_limit.lean

modified theorem add_comm_group.direct_limit.directed_system

Modified src/algebra/module.lean

added theorem add_monoid_hom.map_int_cast_smul

added theorem add_monoid_hom.map_nat_cast_smul

added theorem add_monoid_hom.map_rat_cast_smul

added theorem add_monoid_hom.map_rat_module_smul

deleted theorem add_monoid_hom.map_smul_cast

added def add_monoid_hom.to_int_linear_map

added def add_monoid_hom.to_rat_linear_map

deleted def is_add_group_hom.to_linear_map

deleted theorem module.add_monoid_smul_eq_smul

modified theorem module.gsmul_eq_smul_cast

deleted theorem module.smul_eq_smul

added theorem semimodule.add_monoid_smul_eq_smul

added theorem semimodule.smul_eq_smul