Def add_monoid.End

Modification history

2020-08-03 16:25
src/algebra/group_ring_action.lean
chore(algebra/group_ring_action): docstring, move monoid.End to algebra/group/hom (#3671)
Deleted add_monoid.EndView on Github →
2020-05-01 07:42
src/algebra/group_ring_action.lean
feat(algebra/group_ring_action) define group actions on rings (#2566) …
Added add_monoid.EndView on Github →