Prod, product, sprod

Stream: mathlib4

[Yury G. Kudryashov]

I suggest that we rename lemmas about _ ×ˢ _ to *_sprod_* (creating lots of deprecated aliases). Currently, lemmas for sets, subgroups etc use prod while lemmas for Finset use product to avoid conflict with Finset.prod.

[Yaël Dillies]

Maybe cartProd instead?

[Yury G. Kudryashov]

What does it stand for?

[Yaël Dillies]

"cartesian product"

[Yury G. Kudryashov]

Then we should rename docs#SProd too.

[Yury G. Kudryashov]

But Prod is a cartesian product too, so it doesn't help to disambiguate.

[Yaël Dillies]

Is there any need to disambiguate from docs#Prod ?

[Eric Wieser]

We could rename Finset.prod to Finset.iMul, with the reasoning sup : iSup :: mul : iMul

[Eric Wieser]

More seriously, it's tempting to let the things about Prod claim the prod name, and rename the nary multiplication, with product being the least controversial option I can think of

[Yury G. Kudryashov]

And what about docs#SProd ?

[Eric Wieser]

We have things like LinearMap.prod (as in Prod) to consider too

[Yury G. Kudryashov]

IMHO, we should rename lemmas/defs like docs#LinearMap.prod to prodMk

[Yury G. Kudryashov]

With prodMap docs#Prod.map being another contestant for the name prod here.

[Eric Wieser]

Whoops, prodMap is the one I meant to suggest

[Yury G. Kudryashov]

So, it's not clear from the which one docs#LinearMap.prod is, which is a good reason to rename it.

[Eric Wieser]

If you take the "sets are functions" view, then SProd and prodMap are really the same operation

[Yury G. Kudryashov]

Also, it would be nice to have a common API for these constructions but my attempt at creating a common data structure for *FunLike failed.

[Yury G. Kudryashov]

E.g., it would be nice to have a generic lemma in place of docs#Submonoid.gc_map_comap etc