Documentation

Mathlib.Algebra.Category.AlgebraCat.Monoidal

The monoidal category structure on R-algebras #

@[reducible, inline]
noncomputable abbrev AlgebraCat.instMonoidalCategory.tensorObj {R : Type u} [CommRing R] (X : AlgebraCat R) (Y : AlgebraCat R) :

Auxiliary definition used to fight a timeout when building AlgebraCat.instMonoidalCategory.

Equations
Instances For
    @[reducible, inline]

    Auxiliary definition used to fight a timeout when building AlgebraCat.instMonoidalCategory.

    Equations
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Equations
      • One or more equations did not get rendered due to their size.

      forget₂ (AlgebraCat R) (ModuleCat R) as a monoidal functor.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For