Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-13 06:04 add577d7

View on Github →

feat(group_theory/group_action/defs): add has_mul.to_has_scalar and relax typeclass in smul_mul_smul (#7885)

Estimated changes

modified theorem mul_smul_comm
modified theorem smul_eq_mul
modified theorem smul_mul_assoc
modified theorem smul_mul_smul