Commit 2023-06-05 01:30 208633bf

View on Github →

feat: port CategoryTheory.Monoidal.OfChosenFiniteProducts.Symmetric (#4658)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Symmetric.lean

added theorem CategoryTheory.MonoidalOfChosenFiniteProducts.braiding_naturality

added theorem CategoryTheory.MonoidalOfChosenFiniteProducts.hexagon_forward

added theorem CategoryTheory.MonoidalOfChosenFiniteProducts.hexagon_reverse

added theorem CategoryTheory.MonoidalOfChosenFiniteProducts.symmetry

added def CategoryTheory.symmetricOfChosenFiniteProducts