Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-24 15:08 3f8a492b

View on Github →

chore(category_theory): replace some @[simp] with @[simps] (#1605)

Estimated changes

Modified src/category_theory/limits/shapes/binary_products.lean

modified def category_theory.limits.coprod.associator

modified def category_theory.limits.coprod.braiding

modified def category_theory.limits.coprod.left_unitor

modified def category_theory.limits.coprod.right_unitor

modified def category_theory.limits.prod.associator

modified def category_theory.limits.prod.braiding

modified def category_theory.limits.prod.left_unitor

modified def category_theory.limits.prod.right_unitor