prod vs prod_mk

Stream: new members

[Nicolò Cavalleri]

I see that in most parts of Mathlib (especially for more basic stuff, such as topology) lemmas having to do with the function (λ x, (f x, g x)) are named with prod_mk, whereas in some newer part of mathlib they are named with simply prod (for example there istimes_cont_diff.prod instead of times_cont_diff.prod_mk). I guess the reason for the first name was to distinguish it from prod_map((λ x y, (f x, g y))) to avoid ambiguity. Since I am writing a lot of lemmas on product manifolds, I was wondering if it may be a good idea to look for uniformity in Mathlib on these names or if I can choose freely which convention to adopt.

[Sebastien Gouezel]

Coherence is definitely a good option. As to whether we should use prod_mk or prod, I don't have a strong opinion, but I think I prefer slightly prod as it is shorter, and not really ambiguous.