Mathlib v3 is deprecated. Go to Mathlib v4

Def add_monoid.End.mul_right

Modification history

2022-02-09 18:57

src/algebra/group/hom_instances.lean

feat(algebra.group.hom_instances): Define left and right multiplication operators (#11843) …

Added add_monoid.End.mul_right View on Github →