Theorems · Theorem · category theory

CategoryTheory.MonoidalLinear.smul_whiskerRight

∀ {R : Type u_1} {inst : Semiring R} {C : Type u_2} {inst_1 : CategoryTheory.Category.{v_1, u_2} C}
  {inst_2 : CategoryTheory.Preadditive C} {inst_3 : CategoryTheory.Linear R C}
  {inst_4 : CategoryTheory.MonoidalCategory C} {inst_5 : CategoryTheory.MonoidalPreadditive C}
  [self : CategoryTheory.MonoidalLinear R C] (r : R) {Y Z : C} (f : Y ⟶ Z) (X : C),
  CategoryTheory.MonoidalCategoryStruct.whiskerRight (r • f) X =
    r • CategoryTheory.MonoidalCategoryStruct.whiskerRight f X

Defined in

Mathlib.CategoryTheory.Monoidal.Linear

Cited by

1 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms

Assumes

CategoryTheory.MonoidalLinear