Commit 2023-09-14 07:53 8fa31ad9

View on Github →

feat(CategoryTheory/Limits/Shapes/Biproducts): add associator (#7127) As far as I can tell this doesn't exist anywhere else. The motivation is #7125, but I have a lot less idea of what I'm doing there than I do here.

Estimated changes

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

added def CategoryTheory.Limits.biprod.associator

added theorem CategoryTheory.Limits.biprod.associator_inv_natural

added theorem CategoryTheory.Limits.biprod.associator_natural

modified def CategoryTheory.Limits.biproductBiproductIso