Theorem smul_one_mul
Modification history
2022-08-12 14:28
src/group_theory/group_action/defs.lean
feat(group_theory/group_action/defs): `vadd_assoc_class` (#15844) …
Modified smul_one_mulView on Github →2022-07-01 20:56
src/group_theory/group_action/defs.lean
chore(group_theory/group_action/basic): relax monoid to mul_one_class (#15051)
Modified smul_one_mulView on Github →