Def linear_map.restrict_scalars
Modification history
2021-09-24 06:10
src/algebra/module/linear_map.lean
feat(linear_algebra): redefine `linear_map` and `linear_equiv` to be semilinear (#9272) …
Modified linear_map.restrict_scalarsView on Github →2021-05-27 09:01
src/algebra/module/linear_map.lean
feat(algebra/module/linear_map): `linear_(map|equiv).restrict_scalars` is injective (#7725) …
Modified linear_map.restrict_scalarsView on Github →2021-04-24 15:20
src/algebra/module/linear_map.lean
refactor(*): rename `semimodule` to `module`, delete typeclasses `module` and `vector_space` (#7322) …
Modified linear_map.restrict_scalarsView 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.restrict_scalarsView on Github →2020-10-31 17:41
src/algebra/algebra/basic.lean
chore(group_theory/group_action): introduce `smul_comm_class` (#4770)
Modified linear_map.restrict_scalarsView on Github →2020-10-23 10:15
src/algebra/algebra/basic.lean
refactor(*): use is_scalar_tower instead of restrict_scalars (#4733) …
Modified linear_map.restrict_scalarsView on Github →