Documentation

Mathlib.CategoryTheory.Monoidal.Linear

Linear monoidal categories #

A monoidal category is MonoidalLinear R if it is monoidal preadditive and tensor product of morphisms is R-linear in both factors.

A category is MonoidalLinear R if tensoring is R-linear in both factors.

Instances