Skip to content

Commit

Permalink
fix
Browse files Browse the repository at this point in the history
  • Loading branch information
FR-vdash-bot committed May 11, 2024
1 parent 0712297 commit ba1eb0b
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -666,6 +666,7 @@ theorem rightUnitor_monoidal (X₁ X₂ : C) :
coherence
#align category_theory.right_unitor_monoidal CategoryTheory.rightUnitor_monoidal

set_option maxHeartbeats 400000 in
theorem associator_monoidal (X₁ X₂ X₃ Y₁ Y₂ Y₃ : C) :
tensor_μ C (X₁ ⊗ X₂, X₃) (Y₁ ⊗ Y₂, Y₃) ≫
(tensor_μ C (X₁, X₂) (Y₁, Y₂) ▷ (X₃ ⊗ Y₃)) ≫ (α_ (X₁ ⊗ Y₁) (X₂ ⊗ Y₂) (X₃ ⊗ Y₃)).hom =
Expand Down

0 comments on commit ba1eb0b

Please sign in to comment.