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

Commit
4 years ago
feat(group_theory/group_action/defs): add `has_mul.to_has_scalar` and relax typeclass in `smul_mul_smul` (#7885)
Author
Parents
Loading