mathlib

c6381aa1 - chore(algebra/group_ring_action): docstring, move monoid.End to algebra/group/hom (#3671)