Naming convention for function smul

Stream: general

[Yury G. Kudryashov]

We have 2 SMuls on functions: ((f : α → M) • (g : α → β)) x = f x • g x and ((c : M) • (g : α → β)) x = c • g x. Lemmas about both smuls use smul in the name. Should we use some other string in the lemmas about the first smul?

[Yury G. Kudryashov]

Or use const_smul for the latter one as in docs#Set.indicator_smul and docs#Set.indicator_const_smul ?

[Eric Wieser]

pointwiseSmul?

[Eric Wieser]

It's a pretty bad instance generally, that causes non-eq diamonds

[Eric Wieser]

If we removed it then we wouldn't need to name it any more!

[Anatole Dedecker]

Which instance do you want to remove?

[Eric Wieser]

docs#Pi.smul' is the one that I consider bad, which I explain here.

[Yury G. Kudryashov]

As I explained there, we want this instance for add_torsors but moving it to a scope LGTM.

[Yury G. Kudryashov]

Do you want to move it?