Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-31 17:41 d91c8785

View on Github →

chore(group_theory/group_action): introduce smul_comm_class (#4770)

Estimated changes

Modified src/algebra/algebra/basic.lean

deleted theorem linear_map.algebra_module.smul_apply

deleted def linear_map.restrict_scalars

deleted theorem linear_map.smul_apply'

deleted theorem map_smul_eq_smul_map

Modified src/algebra/module/linear_map.lean

added theorem linear_map.map_smul_of_tower

added def linear_map.restrict_scalars

Modified src/analysis/convex/basic.lean

Modified src/data/complex/module.lean

Modified src/group_theory/group_action.lean

deleted theorem mul_smul

modified theorem smul_assoc

deleted theorem smul_comm

added theorem smul_comm_class.symm

added theorem smul_one_smul

Modified src/linear_algebra/basic.lean

added def linear_map.applyₗ'

modified theorem linear_map.smul_apply

modified theorem linear_map.smul_comp

Modified src/linear_algebra/matrix.lean

Modified src/representation_theory/maschke.lean

Modified src/ring_theory/derivation.lean

Modified src/topology/algebra/module.lean