Theorems · Theorem · category theory

CategoryTheory.RingObj.mul_add

∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.CartesianMonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} (R : C) [self : CategoryTheory.RingObj R],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R CategoryTheory.AddMonObj.add)
      CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R (CategoryTheory.SemiCartesianMonoidalCategory.fst R R))
          CategoryTheory.MonObj.mul)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R (CategoryTheory.SemiCartesianMonoidalCategory.snd R R))
          CategoryTheory.MonObj.mul))
      CategoryTheory.AddMonObj.add

Defined in

Mathlib.CategoryTheory.Monoidal.Ring

Cited by

1 results in Mathlib

Foundations

Depth 27 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.RingObj