Duplicate mul_action defs

Stream: general

[Eric Wieser]

I just realized that the docs#monoid_hom.comp_mul_action def I introduced duplicates docs#mul_action.comp_hom. Which name is better?

[Eric Wieser]

I don't think we have docs#semimodule.comp_hom, but I could rename docs#ring_hom.comp_semimodule

[Yury G. Kudryashov]

I prefer mul_action.comp_hom because we take (\bu) ∘ f, not the other way.

[Yury G. Kudryashov]

I'm going to remove your def in branch#smul-to-add for now. Please tell me if I should revert this.

[Eric Wieser]

The downside of comp_hom is that it doesn't work with dot notation

[Eric Wieser]

But I agree with the order argument

[Eric Wieser]

/poll Which name is better

• mul_action.comp_hom, semimodule.comp_hom (matches the order of composition)
• monoid_hom.comp_mul_action, ring_hom.comp_semimodule (works with dot notation)

[Johan Commelin]

I prefer the first one, but mostly just because I use it most, and hence I'm accustomed to it.

[Anne Baanen]

My intuition says the first one is better, but there is also the family of docs#function.injective.semigroup, which seems to give precendence to the second choice. So I'm officially undecided.

[Eric Wieser]

Since both of you agree with Yury, let's just rename them

[Eric Wieser]

Although it probably makes sense to split that change out of Yury's PR, and possibly to merge #6909 first

[Eric Wieser]

Done in #6942, which folds in #6909 since it's basically all the same anyway.