Mathlib v3 is deprecated. Go to Mathlib v4

Theorem linear_map.map_smul_of_tower

Modification history

2022-06-30 19:45
src/algebra/module/linear_map.lean
refactor(algebra/group/defs): rename has_scalar to has_smul (#14559) …
Modified linear_map.map_smul_of_towerView on Github →
2021-01-06 16:21
src/algebra/module/linear_map.lean
feat(linear_algebra/tensor_product,algebra/module/linear_map): Made tmul_smul and map_smul_of_tower work for int over semirings (#5430) …
Modified linear_map.map_smul_of_towerView on Github →
2020-10-31 17:41
src/algebra/module/linear_map.lean
chore(group_theory/group_action): introduce `smul_comm_class` (#4770)
Added linear_map.map_smul_of_towerView on Github →