Missing coercions

Stream: new members

[Nicolò Cavalleri]

Why do not linear maps extend monoid homomorphisim? I am formalizing derivations and I'd automatically expect that extending linear maps I'd get automatic coerctions to monoid homomorphism, but linear maps were not designed like this and I wonder if there is a reason

[Reid Barton]

Maybe bundled linear maps came before bundled additive monoid maps

[Nicolò Cavalleri]

Is it a good idea to change it?

[Reid Barton]

seems like a good idea to try!

[Yury G. Kudryashov]

Note that we have docs#distrib_mul_action_hom. A good project would be to migrate linear_map`s to this structure.

[Yury G. Kudryashov]

BTW, @Kenny Lau could you please move src#monoid.End to algebra/group/hom and add a module docstring to algebra/group_ring_action?

[Kenny Lau]

@Yury G. Kudryashov #3671

[Yury G. Kudryashov]

Commented