Zulip Chat Archive

Stream: new members

Topic: prod vs prod_mk

view this post on Zulip Nicolò Cavalleri (Jun 29 2020 at 09:05):

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.

view this post on Zulip Sebastien Gouezel (Jun 29 2020 at 09:19):

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.

Last updated: May 08 2021 at 17:33 UTC