Def CategoryTheory.Monoidal.laxToTransported

Modification history

2023-10-09 18:38

Mathlib/CategoryTheory/Monoidal/Transport.lean

feat(CategoryTheory/Monoidal/Transport): generalize to a faithful functor (#7237) …

Deleted CategoryTheory.Monoidal.laxToTransported View on Github →

2023-03-29 09:53

Mathlib/CategoryTheory/Monoidal/Transport.lean

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

Added CategoryTheory.Monoidal.laxToTransported View on Github →