Commit 2023-03-27 13:30 32f816ec

View on Github →

feat: port CategoryTheory.Monoidal.Discrete (#3038)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Monoidal/Discrete.lean

added def CategoryTheory.Discrete.monoidalFunctor

added def CategoryTheory.Discrete.monoidalFunctorComp

added theorem CategoryTheory.Discrete.monoidal_tensorUnit_as