Should `Prod.swap_prod_mk` be renamed to `Prod.swap_prodMk`?

Stream: mathlib4

[Jihoon Hyun]

I see many other prodMks, like docs#IsMin.prodMk , docs#CauchySeq.prodMk , and many more, so I suspect that docs#Prod.swap_prod_mk probably has the deprecated name.

[Yaël Dillies]

Yes, that's correct. #naming says that Prod.mk in a namespace other than Prod should be mk, unless ambiguous (which it is), in which case it becomes prodMk

[Jihoon Hyun]

I just realized that docs#Prod.swap_prod_mk is defined in Init. Does the naming convention still hold?

[Yaël Dillies]

Not really, but that means mathlib probably wants an alias with the correct name