Def CategoryTheory.MonoidalCategory.ofTensorHom

Modification history

2023-10-25 10:47

Mathlib/CategoryTheory/Monoidal/Category.lean

refactor: Move the data fields of `MonoidalCategory` into a `Struct` class (#7279) …

Deleted CategoryTheory.MonoidalCategory.ofTensorHom View on Github →

2023-08-07 12:37

Mathlib/CategoryTheory/Monoidal/Category.lean

feat(CategoryTheory/Monoidal): define whiskering operators (#6420) …

Added CategoryTheory.MonoidalCategory.ofTensorHom View on Github →