basic): `mul_left` is a monoid hom (#17900)

Commit

2 years ago

feat(group_theory/perm/basic): `mul_left` is a monoid hom (#17900) `equiv.mul_left` is a monoid homomorphism.

Author

YaelDillies

Parents