Commit 2024-05-21 15:09 3ab8e581

View on Github →

feat(Category/Theory/Monoidal): monoids in a symmetric category form a symmetric category (#13058)

Estimated changes

Modified Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean

added theorem CategoryTheory.braiding_inv_tensorUnit_left

added theorem CategoryTheory.braiding_inv_tensorUnit_right

Modified Mathlib/CategoryTheory/Monoidal/Mon_.lean

added theorem Mon_.mul_braiding

added theorem Mon_.one_braiding

added theorem Mon_.tensor_mul

added theorem Mon_.tensor_one