Commit 2023-03-29 09:53 44b9073f

View on Github →

feat: port CategoryTheory.Monoidal.Transport (#3151)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Monoidal/Transport.lean

added def CategoryTheory.Monoidal.Transported

added def CategoryTheory.Monoidal.fromTransported

added def CategoryTheory.Monoidal.laxToTransported

added def CategoryTheory.Monoidal.toTransported

added def CategoryTheory.Monoidal.transport

added def CategoryTheory.Monoidal.transportedMonoidalCounitIso

added def CategoryTheory.Monoidal.transportedMonoidalUnitIso