Algebra.Hom.GroupAction mathlib4#1424

Stream: mathlib4

[Johan Commelin]

There's a question on this PR about certain coercions that might no longer be needed.
@Anne Baanen could you please take a look at this?

[Anne Baanen]

I was a few minutes too late but for what it's worth, I believe the issues discussed in this PR have indeed been appropriately resolved :)