Theorems · Theorem · category theory

CategoryTheory.mul_add_iff

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (R : C)
  [inst_2 : CategoryTheory.MonObj R] [inst_3 : CategoryTheory.AddMonObj 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 ↔
    ∀ ⦃X : C⦄ (a b c : X ⟶ R), a * (b + c) = a * b + a * c

Defined in

Mathlib.CategoryTheory.Monoidal.Ring

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CartesianMonoidalCategoryCategoryTheory.MonObjCategoryTheory.AddMonObj