Matrix.dotProduct rename?

Stream: mathlib4

[Martin Dvořák]

One more name that upsets me is docs#Matrix.dotProduct .
First of all, it isn't really about matrix.
Second, the name is too long for such an omnipresent operation.
What do you think about renaming it?

[Martin Dvořák]

/poll What should it be called?
Matrix.dotProduct
dotProduct
Matrix.dot

[Winston Yin (尹維晨)]

May I also suggest making it a sister of SMul by calling it DMul or more transparently dotMul.

Calling it dotProduct will make it consistent with the existing crossProduct, unless both are changed to (something)Mul

[Martin Dvořák]

Embarrassingly, I didn't remember the name of docs#crossProduct even tho I was the one who added it.

[Martin Dvořák]

Now I am even more confident that dotProduct should not be namespaced the way it is now.

[Martin Dvořák]

Martin Dvořák said:

Embarrassingly, I didn't remember the name of docs#crossProduct even tho I was the one who added it.

Ah yeah, that's the weird thing where the definition is called crossProduct but in names of all lemmas cross is used. I wonder if this kind of naming is used anywhere else in Mathlib and if it should be changed.

[Violeta Hernández]

I'm not sure about precedent, but I think this is fine as is. Having cross in the global namespace feels like a mistake.

[Martin Dvořák]

We certainly shouldn't have cross in the global namespace.

[Kim Morrison]

Martin Dvořák said:

Martin Dvořák said:

Embarrassingly, I didn't remember the name of docs#crossProduct even tho I was the one who added it.

Ah yeah, that's the weird thing where the definition is called crossProduct but in names of all lemmas cross is used. I wonder if this kind of naming is used anywhere else in Mathlib and if it should be changed.

Yes, all the lemmas should be renamed to use crossProduct.

[Martin Dvořák]

The consensus is clear so I'll change it to dotProduct soon.

[Martin Dvořák]

#19910

[Martin Dvořák]

Do we want the protected alias thing? Note that normal alias breaks files that open the Matrix namespace.

[Floris van Doorn]

If you are talking about the deprecations: yes, let's keep them for a while using protected alias.

[Martin Dvořák]

Both the definition and the lemmas, right?

[Martin Dvořák]

All right, I doublechecked everything. The only declarations that didn't obtain the alias are dotProduct_single and dotProduct_single_one as they already had deprecation on them. However, please check that these two deprecations are correctly written after the update.

[Martin Dvořák]

Can we speed up #19910 please?