Mathlib v3 is deprecated. Go to Mathlib v4

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.End View 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.End View on Github →