Commit 2024-10-17 07:12 dc48f47d
View on Github →feat(CategoryTheory/Products): an ext lemma for morphisms in product categories (#17721)
Until now, in order to check an identity of morphisms in a product category, we had to do dsimp; ext. Now, ext would also work, which shall ease automation in some future applications.