Commit 2024-09-14 12:37 d3dbb49c

View on Github →

chore: flatten arguments of tensor_μ (#16739)

Estimated changes

Modified Mathlib/Algebra/Category/ModuleCat/Monoidal/Symmetric.lean

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

modified def CategoryTheory.tensor_μ

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

Modified Mathlib/CategoryTheory/Monoidal/Comon_.lean

Modified Mathlib/CategoryTheory/Monoidal/Mon_.lean