prod name

Stream: general

[Patrick Massot]

The map sending y to (x, y) is prod.mk x. Do we have a name for the map sending x to (x, y)? I'd like to name a lemma about this map.

[Floris van Doorn]

maybe prod_mk_right and prod_mk_left? There is docs#set.mk_preimage_prod_left

[Eric Wieser]

We also have docs#linear_map.inl and docs#linear_map.inr for when the fixed x or y are 0

[Scott Morrison]

For products of categories we use sectl.

[Scott Morrison]

https://leanprover-community.github.io/mathlib_docs/category_theory/products/basic.html

[Scott Morrison]

Although this used infrequently enough it is trivial to rename if you pick something else.