Commit 2023-02-28 18:30 62da6140

View on Github →

feat: Port CategoryTheory.Sums.Associator (#2447)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Sums/Associator.lean

added def CategoryTheory.sum.associativity

added def CategoryTheory.sum.associator

added theorem CategoryTheory.sum.associator_map_inl_inl

added theorem CategoryTheory.sum.associator_map_inl_inr

added theorem CategoryTheory.sum.associator_map_inr

added theorem CategoryTheory.sum.associator_obj_inl_inl

added theorem CategoryTheory.sum.associator_obj_inl_inr

added theorem CategoryTheory.sum.associator_obj_inr

added def CategoryTheory.sum.inverseAssociator

added theorem CategoryTheory.sum.inverseAssociator_map_inl

added theorem CategoryTheory.sum.inverseAssociator_map_inr_inl

added theorem CategoryTheory.sum.inverseAssociator_map_inr_inr

added theorem CategoryTheory.sum.inverseAssociator_obj_inl

added theorem CategoryTheory.sum.inverseAssociator_obj_inr_inl

added theorem CategoryTheory.sum.inverseAssociator_obj_inr_inr