Commit 2023-07-31 08:59 2b0e9629

View on Github →

feat: interaction between eqToHom and (co/bi/)products (#6258)

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean

added theorem CategoryTheory.Limits.biproduct.eqToHom_comp_ι

added theorem CategoryTheory.Limits.biproduct.π_comp_eqToHom

Modified Mathlib/CategoryTheory/Limits/Shapes/Products.lean

added theorem CategoryTheory.Limits.Pi.π_comp_eqToHom

added theorem CategoryTheory.Limits.Sigma.eqToHom_comp_ι