Stream: new members
Topic: prod vs prod_mk
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 is
times_cont_diff.prod instead of
times_cont_diff.prod_mk). I guess the reason for the first name was to distinguish it from
(λ 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 (Jun 29 2020 at 09:19):
Coherence is definitely a good option. As to whether we should use
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