Commit 2025-06-22 05:59 61554979

feat(CategoryTheory/Products/Basic): alternative constructor for morphisms in products (#26206) In many instances, constructing morphisms is painful and requires extra type annotations to get lean to accept (f, g) as a valid morphism in a product category. This is an attempt to provide a constructor that works better. See #mathlib4 > product of morphisms in product category