Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-05 07:50 3f26ba88

View on Github →

feat(category_theory/products): associators (#982)

Estimated changes

Created src/category_theory/products/associator.lean

added def category_theory.prod.associativity

added def category_theory.prod.associator

added theorem category_theory.prod.associator_map

added theorem category_theory.prod.associator_obj

added def category_theory.prod.inverse_associator

added theorem category_theory.prod.inverse_associator_map

added theorem category_theory.prod.inverse_associator_obj

Renamed src/category_theory/bifunctor.lean to src/category_theory/products/bifunctor.lean

Renamed src/category_theory/products.lean to src/category_theory/products/default.lean