Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-10 21:07 fa414364

View on Github →

feat(algebra/,group_theory/): instances/lemmas about is_scalar_tower and smul_comm_class (#9533)

Estimated changes

Modified src/algebra/algebra/basic.lean

Modified src/algebra/group/prod.lean

added theorem prod.mul_def

Modified src/algebra/module/basic.lean

Modified src/algebra/opposites.lean

modified theorem opposite.op_smul_eq_mul

Modified src/group_theory/group_action/defs.lean

added theorem is_scalar_tower.of_smul_one_mul

added theorem mul_smul_one

added theorem smul_comm_class.of_mul_smul_one

added theorem smul_one_mul

Modified src/group_theory/group_action/prod.lean

added theorem prod.smul_def