mulLeft vs leftMul vs mul_left

Stream: mathlib4

[Yury G. Kudryashov]

We have docs#Equiv.mulLeft and docs#leftMul
Should we sync the names?

[Yury G. Kudryashov]

Probably, yes. Which one is better?

[Yury G. Kudryashov]

Or should we drop docs#leftMul and docs#rightMul in favor of inline lambdas?

[Yury G. Kudryashov]

@loogle leftMul

[loogle]

:search: leftMul, leftMul.eq_1

[Yury G. Kudryashov]

@loogle rightMul

[loogle]

:search: rightMul, rightMul.eq_1

[Yury G. Kudryashov]

So, these 2 functions are never used in the library.

[Yury G. Kudryashov]

They were added by @Nicolò Cavalleri in !3#3529

[Yury G. Kudryashov]

Also, should we start using mulLeft and mulRight in lemma names pretending that def mulLeft exists and we're talking about it, not fun x => a * x?

[Eric Wieser]

Yury G. Kudryashov said:

They were added by Nicolò Cavalleri in !3#3529

The only uses of these were removed in !3#3641, I think

[Eric Wieser]

Yury G. Kudryashov said:

Or should we drop docs#leftMul and docs#rightMul in favor of inline lambdas?

Deprecated in #23847, especially since we have nice notation for them