Loogle!
Result
Found 132 declarations mentioning CategoryTheory.AddMonObj.add.
- CategoryTheory.AddMonObj.add 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {X : C} [self : CategoryTheory.AddMonObj X] : CategoryTheory.MonoidalCategoryStruct.tensorObj X X ⟶ X - CategoryTheory.AddMonObj.ext 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : C} (h₁ h₂ : CategoryTheory.AddMonObj X) (H : CategoryTheory.AddMonObj.add = CategoryTheory.AddMonObj.add) : h₁ = h₂ - CategoryTheory.AddMonObj.ext_iff 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : C} {h₁ h₂ : CategoryTheory.AddMonObj X} : h₁ = h₂ ↔ CategoryTheory.AddMonObj.add = CategoryTheory.AddMonObj.add - CategoryTheory.AddMonObj.add_def 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.AddMonObj.add = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom - CategoryTheory.IsCommAddMonObj.add_comm 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {inst✝² : CategoryTheory.BraidedCategory C} (X : C) {inst✝³ : CategoryTheory.AddMonObj X} [self : CategoryTheory.IsCommAddMonObj X] : CategoryTheory.CategoryStruct.comp (β_ X X).hom CategoryTheory.AddMonObj.add = CategoryTheory.AddMonObj.add - CategoryTheory.IsCommAddMonObj.add_comm' 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M : C) [CategoryTheory.AddMonObj M] [CategoryTheory.BraidedCategory C] [CategoryTheory.IsCommAddMonObj M] : CategoryTheory.CategoryStruct.comp (β_ M M).inv CategoryTheory.AddMonObj.add = CategoryTheory.AddMonObj.add - CategoryTheory.AddMon.trivial_addMon_add 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.AddMonObj.add = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom - CategoryTheory.IsCommAddMonObj.mk 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X : C} [CategoryTheory.AddMonObj X] (add_comm : CategoryTheory.CategoryStruct.comp (β_ X X).hom CategoryTheory.AddMonObj.add = CategoryTheory.AddMonObj.add := by cat_disch) : CategoryTheory.IsCommAddMonObj X - CategoryTheory.IsAddMonHom.add_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {M' N' : C} {inst✝² : CategoryTheory.AddMonObj M'} {inst✝³ : CategoryTheory.AddMonObj N'} (f : M' ⟶ N') [self : CategoryTheory.IsAddMonHom f] : CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f f) CategoryTheory.AddMonObj.add - CategoryTheory.AddMonObj.add_zero 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} (X : C) [self : CategoryTheory.AddMonObj X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.AddMonObj.zero) CategoryTheory.AddMonObj.add = (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom - CategoryTheory.AddMonObj.zero_add 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} (X : C) [self : CategoryTheory.AddMonObj X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.AddMonObj.zero X) CategoryTheory.AddMonObj.add = (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom - CategoryTheory.AddMonObj.ofIso_add 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M X : C} [CategoryTheory.AddMonObj M] (e : M ≅ X) : CategoryTheory.AddMonObj.add = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.inv e.inv) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add e.hom) - CategoryTheory.Mathlib.Tactic.MonTauto.eq_add_zero 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : C} [CategoryTheory.AddMonObj M] : (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id M) CategoryTheory.AddMonObj.zero) CategoryTheory.AddMonObj.add - CategoryTheory.Mathlib.Tactic.MonTauto.eq_zero_add 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : C} [CategoryTheory.AddMonObj M] : (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.zero (CategoryTheory.CategoryStruct.id M)) CategoryTheory.AddMonObj.add - CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidalObj_μ 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.AddMon C) (X Y : CategoryTheory.Discrete PUnit.{u_1 + 1}) : CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidalObj A) X Y = CategoryTheory.AddMonObj.add - CategoryTheory.Mathlib.Tactic.MonTauto.leftUnitor_neg_zero_tensor_add 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M X₁ : C} [CategoryTheory.AddMonObj M] (f : X₁ ⟶ M) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X₁).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.zero f) CategoryTheory.AddMonObj.add) = f - CategoryTheory.Mathlib.Tactic.MonTauto.rightUnitor_neg_tensor_zero_add 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M X₁ : C} [CategoryTheory.AddMonObj M] (f : X₁ ⟶ M) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X₁).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f CategoryTheory.AddMonObj.zero) CategoryTheory.AddMonObj.add) = f - CategoryTheory.IsCommAddMonObj.add_comm'_assoc 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M : C) [CategoryTheory.AddMonObj M] [CategoryTheory.BraidedCategory C] [CategoryTheory.IsCommAddMonObj M] {Z : C} (h : M ⟶ Z) : CategoryTheory.CategoryStruct.comp (β_ M M).inv (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h) = CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h - CategoryTheory.AddMonObj.add_zero_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : C} [CategoryTheory.AddMonObj M] {Z : C} (f : Z ⟶ M) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f CategoryTheory.AddMonObj.zero) CategoryTheory.AddMonObj.add = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Z).hom f - CategoryTheory.AddMonObj.zero_add_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : C} [CategoryTheory.AddMonObj M] {Z : C} (f : Z ⟶ M) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.zero f) CategoryTheory.AddMonObj.add = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).hom f - CategoryTheory.IsAddMonHom.add_hom_assoc 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {M' N' : C} {inst✝² : CategoryTheory.AddMonObj M'} {inst✝³ : CategoryTheory.AddMonObj N'} (f : M' ⟶ N') [self : CategoryTheory.IsAddMonHom f] {Z : C} (h : N' ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f f) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h) - CategoryTheory.AddMon.tensorAddUnit_add 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.AddMonObj.add = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom - CategoryTheory.Functor.FullyFaithful.addMonObj_add 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.Functor C D} [F.OplaxMonoidal] (hF : F.FullyFaithful) (X : C) [CategoryTheory.AddMonObj (F.obj X)] : CategoryTheory.AddMonObj.add = hF.preimage (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X X) CategoryTheory.AddMonObj.add) - CategoryTheory.IsAddMonHom.mk 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M' N' : C} [CategoryTheory.AddMonObj M'] [CategoryTheory.AddMonObj N'] {f : M' ⟶ N'} (zero_hom : CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero f = CategoryTheory.AddMonObj.zero := by cat_disch) (add_hom : CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f f) CategoryTheory.AddMonObj.add := by cat_disch) : CategoryTheory.IsAddMonHom f - CategoryTheory.Functor.obj.σ_def 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.Functor C D} [F.LaxMonoidal] (X : C) [CategoryTheory.AddMonObj X] : CategoryTheory.AddMonObj.add = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X X) (F.map CategoryTheory.AddMonObj.add) - CategoryTheory.AddMonObj.add_zero_assoc 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} (X : C) [self : CategoryTheory.AddMonObj X] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.AddMonObj.zero) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom h - CategoryTheory.AddMonObj.zero_add_assoc 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} (X : C) [self : CategoryTheory.AddMonObj X] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.AddMonObj.zero X) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom h - CategoryTheory.Mathlib.Tactic.MonTauto.leftUnitor_neg_zero_tensor_add_assoc 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M X₁ : C} [CategoryTheory.AddMonObj M] (f : X₁ ⟶ M) {Z : C} (h : M ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X₁).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.zero f) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h)) = CategoryTheory.CategoryStruct.comp f h - CategoryTheory.Mathlib.Tactic.MonTauto.rightUnitor_neg_tensor_zero_add_assoc 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M X₁ : C} [CategoryTheory.AddMonObj M] (f : X₁ ⟶ M) {Z : C} (h : M ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X₁).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f CategoryTheory.AddMonObj.zero) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h)) = CategoryTheory.CategoryStruct.comp f h - CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_inverse_obj_laxMonoidal_μ 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.AddMon C) (x✝ x✝¹ : CategoryTheory.Discrete PUnit.{w + 1}) : CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidalObj A) x✝ x✝¹ = CategoryTheory.AddMonObj.add - CategoryTheory.AddMonObj.add_zero_hom_assoc 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : C} [CategoryTheory.AddMonObj M] {Z : C} (f : Z ⟶ M) {Z✝ : C} (h : M ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f CategoryTheory.AddMonObj.zero) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Z).hom (CategoryTheory.CategoryStruct.comp f h) - CategoryTheory.AddMonObj.zero_add_hom_assoc 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : C} [CategoryTheory.AddMonObj M] {Z : C} (f : Z ⟶ M) {Z✝ : C} (h : M ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.zero f) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).hom (CategoryTheory.CategoryStruct.comp f h) - CategoryTheory.AddMonObj.tensorObj.add_def 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : C} [CategoryTheory.AddMonObj M] [CategoryTheory.AddMonObj N] : CategoryTheory.AddMonObj.add = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N) (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add) - CategoryTheory.Functor.obj.σ_def_assoc 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.Functor C D} [F.LaxMonoidal] (X : C) [CategoryTheory.AddMonObj X] {Z : D} (h : F.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X X) (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.AddMonObj.add) h) - CategoryTheory.AddMonObj.add_assoc 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} (X : C) [self : CategoryTheory.AddMonObj X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.AddMonObj.add X) CategoryTheory.AddMonObj.add = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X X X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.AddMonObj.add) CategoryTheory.AddMonObj.add) - CategoryTheory.AddMonObj.add_assoc_flip 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M : C) [CategoryTheory.AddMonObj M] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M CategoryTheory.AddMonObj.add) CategoryTheory.AddMonObj.add = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M M M).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.AddMonObj.add M) CategoryTheory.AddMonObj.add) - CategoryTheory.Functor.mapAddMon_obj_addMon_add 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C D) [F.LaxMonoidal] (A : CategoryTheory.AddMon C) : CategoryTheory.AddMonObj.add = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F A.X A.X) (F.map CategoryTheory.AddMonObj.add) - CategoryTheory.AddMon.add_def 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : C} [CategoryTheory.AddMonObj M] [CategoryTheory.AddMonObj N] : CategoryTheory.AddMonObj.add = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N) (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add) - CategoryTheory.AddMon.Hom.mk' 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : CategoryTheory.AddMon C} (f : M.X ⟶ N.X) (zero_f : CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero f = CategoryTheory.AddMonObj.zero := by cat_disch) (add_f : CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f f) CategoryTheory.AddMonObj.add := by cat_disch) : M.Hom N - CategoryTheory.Functor.id_mapAddMon_add 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.AddMon C) : CategoryTheory.AddMonObj.add = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X.X X.X)) CategoryTheory.AddMonObj.add - CategoryTheory.AddMonObj.add_add_add_comm 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M : C) [CategoryTheory.AddMonObj M] [CategoryTheory.BraidedCategory C] [CategoryTheory.IsCommAddMonObj M] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M M M M) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add) CategoryTheory.AddMonObj.add) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add) CategoryTheory.AddMonObj.add - CategoryTheory.AddMonObj.add_add_add_comm' 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M : C) [CategoryTheory.AddMonObj M] [CategoryTheory.BraidedCategory C] [CategoryTheory.IsCommAddMonObj M] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorδ M M M M) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add) CategoryTheory.AddMonObj.add) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add) CategoryTheory.AddMonObj.add - CategoryTheory.AddMonObj.add_assoc_assoc 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} (X : C) [self : CategoryTheory.AddMonObj X] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.AddMonObj.add X) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X X X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.AddMonObj.add) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h)) - CategoryTheory.AddMonObj.add_assoc_flip_assoc 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M : C) [CategoryTheory.AddMonObj M] {Z : C} (h : M ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M CategoryTheory.AddMonObj.add) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M M M).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.AddMonObj.add M) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h)) - CategoryTheory.Mathlib.Tactic.MonTauto.add_assoc_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M X : C} [CategoryTheory.AddMonObj M] (f : X ⟶ M) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X M M).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f CategoryTheory.AddMonObj.add) CategoryTheory.AddMonObj.add) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.CategoryStruct.id M)) CategoryTheory.AddMonObj.add) (CategoryTheory.CategoryStruct.id M)) CategoryTheory.AddMonObj.add - CategoryTheory.Mathlib.Tactic.MonTauto.add_assoc_neg 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M X : C} [CategoryTheory.AddMonObj M] (f : X ⟶ M) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M M X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add f) CategoryTheory.AddMonObj.add) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id M) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id M) f) CategoryTheory.AddMonObj.add)) CategoryTheory.AddMonObj.add - CategoryTheory.AddMon.mkIso 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M N : CategoryTheory.AddMon C} (e : M.X ≅ N.X) (zero_f : CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero e.hom = CategoryTheory.AddMonObj.zero := by cat_disch) (add_f : CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add e.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom) CategoryTheory.AddMonObj.add := by cat_disch) : M ≅ N - CategoryTheory.AddMonObj.add_add_add_comm'_assoc 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M : C) [CategoryTheory.AddMonObj M] [CategoryTheory.BraidedCategory C] [CategoryTheory.IsCommAddMonObj M] {Z : C} (h : M ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorδ M M M M) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h) - CategoryTheory.AddMonObj.add_add_add_comm_assoc 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M : C) [CategoryTheory.AddMonObj M] [CategoryTheory.BraidedCategory C] [CategoryTheory.IsCommAddMonObj M] {Z : C} (h : M ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M M M M) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h) - CategoryTheory.AddMon.tensorObj_add 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : CategoryTheory.AddMon C) : CategoryTheory.AddMonObj.add = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ X.X Y.X X.X Y.X) (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add) - CategoryTheory.AddMon.tensor_add 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M N : CategoryTheory.AddMon C) : CategoryTheory.AddMonObj.add = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M.X N.X M.X N.X) (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add) - CategoryTheory.Mathlib.Tactic.MonTauto.add_assoc_hom_assoc 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M X : C} [CategoryTheory.AddMonObj M] (f : X ⟶ M) {Z : C} (h : M ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X M M).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f CategoryTheory.AddMonObj.add) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.CategoryStruct.id M)) CategoryTheory.AddMonObj.add) (CategoryTheory.CategoryStruct.id M)) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h) - CategoryTheory.Mathlib.Tactic.MonTauto.add_assoc_neg_assoc 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M X : C} [CategoryTheory.AddMonObj M] (f : X ⟶ M) {Z : C} (h : M ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M M X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add f) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id M) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id M) f) CategoryTheory.AddMonObj.add)) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h) - CategoryTheory.AddMonObj.add_braiding 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] (X Y : C) [CategoryTheory.AddMonObj X] [CategoryTheory.AddMonObj Y] : CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add (β_ X Y).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (β_ X Y).hom (β_ X Y).hom) CategoryTheory.AddMonObj.add - CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_functor_obj_addMon_add 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (F : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C) : CategoryTheory.AddMonObj.add = CategoryTheory.Functor.LaxMonoidal.μ F.toFunctor (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Discrete PUnit.{w + 1})) (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Discrete PUnit.{w + 1})) - CategoryTheory.AddMonObj.AddMon_tensor_add_zero 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M N : C) [CategoryTheory.AddMonObj M] [CategoryTheory.AddMonObj N] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj M N) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.zero CategoryTheory.AddMonObj.zero))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N) (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add)) = (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)).hom - CategoryTheory.AddMonObj.AddMon_tensor_zero_add 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M N : C) [CategoryTheory.AddMonObj M] [CategoryTheory.AddMonObj N] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.zero CategoryTheory.AddMonObj.zero)) (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N) (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add)) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)).hom - CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidal_laxMonoidalToAddMon_obj_add 📋 Mathlib.CategoryTheory.Monoidal.Mon
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (F : CategoryTheory.AddMon C) : CategoryTheory.AddMonObj.add = CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add (CategoryTheory.CategoryStruct.id F.X) - CategoryTheory.AddMonObj.add_leftUnitor 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M : C} [CategoryTheory.AddMonObj M] : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) M (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) M) (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom CategoryTheory.AddMonObj.add)) (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).hom) CategoryTheory.AddMonObj.add - CategoryTheory.AddMonObj.add_rightUnitor 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M : C} [CategoryTheory.AddMonObj M] : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) M (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom)) (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).hom) CategoryTheory.AddMonObj.add - CategoryTheory.Functor.comp_mapAddMon_add 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [F.LaxMonoidal] [G.LaxMonoidal] (X : CategoryTheory.AddMon C) : CategoryTheory.AddMonObj.add = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ (F.comp G) X.X X.X) ((F.comp G).map CategoryTheory.AddMonObj.add) - CategoryTheory.AddMonObj.AddMon_tensor_add_assoc 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M N : C) [CategoryTheory.AddMonObj M] [CategoryTheory.AddMonObj N] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N) (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add)) (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N) (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj M N) (CategoryTheory.MonoidalCategoryStruct.tensorObj M N) (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj M N) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N) (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N) (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add))) - CategoryTheory.AddMonObj.add_associator 📋 Mathlib.CategoryTheory.Monoidal.Mon
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N P : C} [CategoryTheory.AddMonObj M] [CategoryTheory.AddMonObj N] [CategoryTheory.AddMonObj P] : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ (CategoryTheory.MonoidalCategoryStruct.tensorObj M N) P (CategoryTheory.MonoidalCategoryStruct.tensorObj M N) P) (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N) (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add)) CategoryTheory.AddMonObj.add)) (CategoryTheory.MonoidalCategoryStruct.associator M N P).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.associator M N P).hom (CategoryTheory.MonoidalCategoryStruct.associator M N P).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M (CategoryTheory.MonoidalCategoryStruct.tensorObj N P) M (CategoryTheory.MonoidalCategoryStruct.tensorObj N P)) (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ N P N P) (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add)))) - CategoryTheory.AddMonObj.instIsAddMonHomAddOfIsCommAddMonObj 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M : C} [CategoryTheory.AddMonObj M] [CategoryTheory.BraidedCategory C] [CategoryTheory.IsCommAddMonObj M] : CategoryTheory.IsAddMonHom CategoryTheory.AddMonObj.add - CategoryTheory.AddMonObj.lift_comp_zero_left 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [CategoryTheory.AddMonObj B] (f : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (g : A ⟶ B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp f CategoryTheory.AddMonObj.zero) g) CategoryTheory.AddMonObj.add = g - CategoryTheory.AddMonObj.lift_comp_zero_right 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [CategoryTheory.AddMonObj B] (f : A ⟶ B) (g : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f (CategoryTheory.CategoryStruct.comp g CategoryTheory.AddMonObj.zero)) CategoryTheory.AddMonObj.add = f - CategoryTheory.Hom.add_def 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {M X : C} [CategoryTheory.AddMonObj M] (f₁ f₂ : X ⟶ M) : f₁ + f₂ = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f₁ f₂) CategoryTheory.AddMonObj.add - CategoryTheory.AddMonObj.lift_comp_zero_left_assoc 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [CategoryTheory.AddMonObj B] (f : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (g : A ⟶ B) {Z : C} (h : B ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp f CategoryTheory.AddMonObj.zero) g) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h) = CategoryTheory.CategoryStruct.comp g h - CategoryTheory.AddMonObj.lift_comp_zero_right_assoc 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [CategoryTheory.AddMonObj B] (f : A ⟶ B) (g : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) {Z : C} (h : B ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f (CategoryTheory.CategoryStruct.comp g CategoryTheory.AddMonObj.zero)) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h) = CategoryTheory.CategoryStruct.comp f h - CategoryTheory.AddMonObj.lift_lift_assoc 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [CategoryTheory.AddMonObj B] (f g h : A ⟶ B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f g) CategoryTheory.AddMonObj.add) h) CategoryTheory.AddMonObj.add = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f (CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift g h) CategoryTheory.AddMonObj.add)) CategoryTheory.AddMonObj.add - CategoryTheory.AddMonObj.add_eq_add 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] (M : C) [CategoryTheory.AddMonObj M] : CategoryTheory.AddMonObj.add = CategoryTheory.SemiCartesianMonoidalCategory.fst M M + CategoryTheory.SemiCartesianMonoidalCategory.snd M M - CategoryTheory.AddMon.hom_add 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : CategoryTheory.AddMon C) [CategoryTheory.IsCommAddMonObj M.X] : CategoryTheory.AddMonObj.add.hom = CategoryTheory.AddMonObj.add - CategoryTheory.AddMonObj.ofRepresentableBy_add 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] (X : C) (F : CategoryTheory.Functor Cᵒᵖ AddMonCat) (α : (F.comp (CategoryTheory.forget AddMonCat)).RepresentableBy X) : CategoryTheory.AddMonObj.add = α.homEquiv'.symm (α.homEquiv' (CategoryTheory.SemiCartesianMonoidalCategory.fst X X) + α.homEquiv' (CategoryTheory.SemiCartesianMonoidalCategory.snd X X)) - CategoryTheory.AddGrpObj.left_neg 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.CartesianMonoidalCategory C} (X : C) [self : CategoryTheory.AddGrpObj X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift CategoryTheory.AddGrpObj.neg (CategoryTheory.CategoryStruct.id X)) CategoryTheory.AddMonObj.add = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X) CategoryTheory.AddMonObj.zero - CategoryTheory.AddGrpObj.right_neg 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.CartesianMonoidalCategory C} (X : C) [self : CategoryTheory.AddGrpObj X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id X) CategoryTheory.AddGrpObj.neg) CategoryTheory.AddMonObj.add = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X) CategoryTheory.AddMonObj.zero - CategoryTheory.AddGrpObj.addRight_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A : C} [CategoryTheory.AddGrpObj A] (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ A) : (CategoryTheory.AddGrpObj.addRight f).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id A) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A) f)) CategoryTheory.AddMonObj.add - CategoryTheory.AddGrpObj.lift_comp_neg_left 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [CategoryTheory.AddGrpObj B] (f : A ⟶ B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp f CategoryTheory.AddGrpObj.neg) f) CategoryTheory.AddMonObj.add = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A) CategoryTheory.AddMonObj.zero - CategoryTheory.AddGrpObj.lift_comp_neg_right 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [CategoryTheory.AddGrpObj B] (f : A ⟶ B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f (CategoryTheory.CategoryStruct.comp f CategoryTheory.AddGrpObj.neg)) CategoryTheory.AddMonObj.add = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A) CategoryTheory.AddMonObj.zero - CategoryTheory.AddGrpObj.lift_left_add_ext 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [CategoryTheory.AddGrpObj B] {f g : A ⟶ B} (i : A ⟶ B) (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f i) CategoryTheory.AddMonObj.add = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift g i) CategoryTheory.AddMonObj.add) : f = g - CategoryTheory.AddGrpObj.addRight_inv 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A : C} [CategoryTheory.AddGrpObj A] (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ A) : (CategoryTheory.AddGrpObj.addRight f).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id A) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A) (CategoryTheory.CategoryStruct.comp f CategoryTheory.AddGrpObj.neg))) CategoryTheory.AddMonObj.add - CategoryTheory.AddGrpObj.lift_neg_comp_left 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [CategoryTheory.AddGrpObj A] [CategoryTheory.AddGrpObj B] (f : A ⟶ B) [CategoryTheory.IsAddMonHom f] : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.AddGrpObj.neg f) f) CategoryTheory.AddMonObj.add = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A) CategoryTheory.AddMonObj.zero - CategoryTheory.AddGrpObj.lift_neg_comp_right 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [CategoryTheory.AddGrpObj A] [CategoryTheory.AddGrpObj B] (f : A ⟶ B) [CategoryTheory.IsAddMonHom f] : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f (CategoryTheory.CategoryStruct.comp CategoryTheory.AddGrpObj.neg f)) CategoryTheory.AddMonObj.add = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A) CategoryTheory.AddMonObj.zero - CategoryTheory.AddGrpObj.eq_lift_neg_left 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [CategoryTheory.AddGrpObj B] (f g h : A ⟶ B) : f = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp g CategoryTheory.AddGrpObj.neg) h) CategoryTheory.AddMonObj.add ↔ CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift g f) CategoryTheory.AddMonObj.add = h - CategoryTheory.AddGrpObj.eq_lift_neg_right 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [CategoryTheory.AddGrpObj B] (f g h : A ⟶ B) : f = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift g (CategoryTheory.CategoryStruct.comp h CategoryTheory.AddGrpObj.neg)) CategoryTheory.AddMonObj.add ↔ CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f h) CategoryTheory.AddMonObj.add = g - CategoryTheory.AddGrpObj.lift_neg_left_eq 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [CategoryTheory.AddGrpObj B] (f g h : A ⟶ B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp f CategoryTheory.AddGrpObj.neg) g) CategoryTheory.AddMonObj.add = h ↔ g = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f h) CategoryTheory.AddMonObj.add - CategoryTheory.AddGrpObj.lift_neg_right_eq 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [CategoryTheory.AddGrpObj B] (f g h : A ⟶ B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f (CategoryTheory.CategoryStruct.comp g CategoryTheory.AddGrpObj.neg)) CategoryTheory.AddMonObj.add = h ↔ f = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift h g) CategoryTheory.AddMonObj.add - CategoryTheory.AddGrpObj.ofIso_add 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {G' X : C} [CategoryTheory.AddGrpObj G'] (e : G' ≅ X) : CategoryTheory.AddMonObj.add = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.inv e.inv) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add e.hom) - CategoryTheory.AddGrpObj.left_neg_assoc 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.CartesianMonoidalCategory C} (X : C) [self : CategoryTheory.AddGrpObj X] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift CategoryTheory.AddGrpObj.neg (CategoryTheory.CategoryStruct.id X)) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero h) - CategoryTheory.AddGrpObj.right_neg_assoc 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.CartesianMonoidalCategory C} (X : C) [self : CategoryTheory.AddGrpObj X] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id X) CategoryTheory.AddGrpObj.neg) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero h) - CategoryTheory.AddGrp.tensorAddUnit_add 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.AddMonObj.add = CategoryTheory.AddMonObj.add - CategoryTheory.AddGrpObj.lift_comp_neg_left_assoc 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [CategoryTheory.AddGrpObj B] (f : A ⟶ B) {Z : C} (h : B ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp f CategoryTheory.AddGrpObj.neg) f) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero h) - CategoryTheory.AddGrpObj.lift_comp_neg_right_assoc 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [CategoryTheory.AddGrpObj B] (f : A ⟶ B) {Z : C} (h : B ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f (CategoryTheory.CategoryStruct.comp f CategoryTheory.AddGrpObj.neg)) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero h) - CategoryTheory.AddGrp.trivial_addGrp_add 📋 Mathlib.CategoryTheory.Monoidal.Grp
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] : CategoryTheory.AddMonObj.add = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom - CategoryTheory.AddGrpObj.lift_neg_comp_left_assoc 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [CategoryTheory.AddGrpObj A] [CategoryTheory.AddGrpObj B] (f : A ⟶ B) [CategoryTheory.IsAddMonHom f] {Z : C} (h : B ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.AddGrpObj.neg f) f) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero h) - CategoryTheory.AddGrpObj.lift_neg_comp_right_assoc 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [CategoryTheory.AddGrpObj A] [CategoryTheory.AddGrpObj B] (f : A ⟶ B) [CategoryTheory.IsAddMonHom f] {Z : C} (h : B ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f (CategoryTheory.CategoryStruct.comp CategoryTheory.AddGrpObj.neg f)) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero h) - CategoryTheory.AddGrpObj.mk 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {X : C} [toAddMonObj : CategoryTheory.AddMonObj X] (neg : X ⟶ X) (left_neg : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift neg (CategoryTheory.CategoryStruct.id X)) CategoryTheory.AddMonObj.add = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X) CategoryTheory.AddMonObj.zero := by cat_disch) (right_neg : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id X) neg) CategoryTheory.AddMonObj.add = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X) CategoryTheory.AddMonObj.zero := by cat_disch) : CategoryTheory.AddGrpObj X - CategoryTheory.AddGrpObj.add_neg 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : C) [CategoryTheory.AddGrpObj A] : CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add CategoryTheory.AddGrpObj.neg = CategoryTheory.CategoryStruct.comp (β_ A A).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddGrpObj.neg CategoryTheory.AddGrpObj.neg) CategoryTheory.AddMonObj.add) - CategoryTheory.AddGrpObj.add_neg_rev 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G : C) [CategoryTheory.AddGrpObj G] : CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add CategoryTheory.AddGrpObj.neg = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddGrpObj.neg CategoryTheory.AddGrpObj.neg) (CategoryTheory.CategoryStruct.comp (β_ G G).hom CategoryTheory.AddMonObj.add) - CategoryTheory.AddGrpObj.tensorHom_neg_neg_add 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : C) [CategoryTheory.AddGrpObj A] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddGrpObj.neg CategoryTheory.AddGrpObj.neg) CategoryTheory.AddMonObj.add = CategoryTheory.CategoryStruct.comp (β_ A A).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add CategoryTheory.AddGrpObj.neg) - CategoryTheory.AddGrp.tensorObj_add 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G H : CategoryTheory.AddGrp C) : CategoryTheory.AddMonObj.add = CategoryTheory.AddMonObj.add - CategoryTheory.Functor.FullyFaithful.addGrpObj_add 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.CartesianMonoidalCategory D] {F : CategoryTheory.Functor C D} [F.Monoidal] (hF : F.FullyFaithful) (X : C) [CategoryTheory.AddGrpObj (F.obj X)] : CategoryTheory.AddMonObj.add = hF.preimage (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X X) CategoryTheory.AddMonObj.add) - CategoryTheory.AddGrp.forget₂AddMon_obj_add 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (A : CategoryTheory.AddGrp C) : CategoryTheory.AddMonObj.add = CategoryTheory.AddMonObj.add - CategoryTheory.AddGrpObj.add_neg_assoc 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : C) [CategoryTheory.AddGrpObj A] {Z : C} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add (CategoryTheory.CategoryStruct.comp CategoryTheory.AddGrpObj.neg h) = CategoryTheory.CategoryStruct.comp (β_ A A).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddGrpObj.neg CategoryTheory.AddGrpObj.neg) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h)) - CategoryTheory.AddGrpObj.add_neg_rev_assoc 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G : C) [CategoryTheory.AddGrpObj G] {Z : C} (h : G ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add (CategoryTheory.CategoryStruct.comp CategoryTheory.AddGrpObj.neg h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddGrpObj.neg CategoryTheory.AddGrpObj.neg) (CategoryTheory.CategoryStruct.comp (β_ G G).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h)) - CategoryTheory.AddGrpObj.tensorHom_neg_neg_add_assoc 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : C) [CategoryTheory.AddGrpObj A] {Z : C} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddGrpObj.neg CategoryTheory.AddGrpObj.neg) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h) = CategoryTheory.CategoryStruct.comp (β_ A A).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add (CategoryTheory.CategoryStruct.comp CategoryTheory.AddGrpObj.neg h)) - CategoryTheory.Functor.mapAddGrp_obj_addGrp_add 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.CartesianMonoidalCategory D] (F : CategoryTheory.Functor C D) [F.Monoidal] (A : CategoryTheory.AddGrp C) : CategoryTheory.AddMonObj.add = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F A.X A.X) (F.map CategoryTheory.AddMonObj.add) - CategoryTheory.AddGrpObj.isPullback 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (A : C) [CategoryTheory.AddGrpObj A] : CategoryTheory.IsPullback (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.AddMonObj.add A) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A A).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A CategoryTheory.AddMonObj.add)) CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add - CategoryTheory.AddGrp.homMk'' 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : CategoryTheory.AddGrp C} (f : A.X ⟶ B.X) (zero_f : CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero f = CategoryTheory.AddMonObj.zero := by cat_disch) (add_f : CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f f) CategoryTheory.AddMonObj.add := by cat_disch) : A ⟶ B - CategoryTheory.Functor.mapAddGrp_id_add 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (A : CategoryTheory.AddGrp C) : CategoryTheory.AddMonObj.add = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj A.X A.X)) CategoryTheory.AddMonObj.add - CategoryTheory.AddGrp.mkIso 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {G H : CategoryTheory.AddGrp C} (e : G.X ≅ H.X) (zero_f : CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero e.hom = CategoryTheory.AddMonObj.zero := by cat_disch) (add_f : CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add e.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom) CategoryTheory.AddMonObj.add := by cat_disch) : G ≅ H - CategoryTheory.AddGrp.homMk''_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : CategoryTheory.AddGrp C} (f : A.X ⟶ B.X) (zero_f : CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero f = CategoryTheory.AddMonObj.zero := by cat_disch) (add_f : CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f f) CategoryTheory.AddMonObj.add := by cat_disch) : (CategoryTheory.AddGrp.homMk'' f zero_f add_f).hom.hom = f - CategoryTheory.AddGrp.mkIso_hom_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {G H : CategoryTheory.AddGrp C} (e : G.X ≅ H.X) (zero_f : CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero e.hom = CategoryTheory.AddMonObj.zero := by cat_disch) (add_f : CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add e.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom) CategoryTheory.AddMonObj.add := by cat_disch) : (CategoryTheory.AddGrp.mkIso e zero_f add_f).hom.hom.hom = e.hom - CategoryTheory.AddGrp.mkIso_inv_hom_hom 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {G H : CategoryTheory.AddGrp C} (e : G.X ≅ H.X) (zero_f : CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero e.hom = CategoryTheory.AddMonObj.zero := by cat_disch) (add_f : CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add e.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom) CategoryTheory.AddMonObj.add := by cat_disch) : (CategoryTheory.AddGrp.mkIso e zero_f add_f).inv.hom.hom = e.inv - CategoryTheory.Functor.comp_mapAddGrp_add 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.CartesianMonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.CartesianMonoidalCategory E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [F.Monoidal] [G.Monoidal] (A : CategoryTheory.AddGrp C) : CategoryTheory.AddMonObj.add = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ (F.comp G) A.X A.X) ((F.comp G).map CategoryTheory.AddMonObj.add) - CategoryTheory.Functor.comp_mapAddGrp_add_assoc 📋 Mathlib.CategoryTheory.Monoidal.Grp
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.CartesianMonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.CartesianMonoidalCategory E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [F.Monoidal] [G.Monoidal] (A : CategoryTheory.AddGrp C) {Z : E} (h : ((F.comp G).mapAddGrp.obj A).X ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ (F.comp G) A.X A.X) (G.map (F.map CategoryTheory.AddMonObj.add))) h - CategoryTheory.AddGrp.hom_add 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (H : CategoryTheory.AddGrp C) [CategoryTheory.IsCommAddMonObj H.X] : CategoryTheory.AddMonObj.add.hom.hom = CategoryTheory.AddMonObj.add - CategoryTheory.AddMod.regular_addMod_vadd 📋 Mathlib.CategoryTheory.Monoidal.Mod
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : C) [CategoryTheory.AddMonObj A] : CategoryTheory.AddModObj.vadd = CategoryTheory.AddMonObj.add - CategoryTheory.AddModObj.vadd_eq_add 📋 Mathlib.CategoryTheory.Monoidal.Mod
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M : C) [CategoryTheory.AddMonObj M] : CategoryTheory.AddModObj.vadd = CategoryTheory.AddMonObj.add - CategoryTheory.AddModObj.add_vadd_self 📋 Mathlib.CategoryTheory.Monoidal.Mod
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M : C) [CategoryTheory.AddMonObj M] (X : C) [CategoryTheory.AddModObj M X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.AddMonObj.add X) CategoryTheory.AddModObj.vadd = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M M X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M CategoryTheory.AddModObj.vadd) CategoryTheory.AddModObj.vadd) - CategoryTheory.AddModObj.add_vadd_self_flip 📋 Mathlib.CategoryTheory.Monoidal.Mod
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : C} [CategoryTheory.AddMonObj M] (X : C) [CategoryTheory.AddModObj M X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M CategoryTheory.AddModObj.vadd) CategoryTheory.AddModObj.vadd = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M M X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.AddMonObj.add X) CategoryTheory.AddModObj.vadd) - CategoryTheory.AddModObj.add_vadd_self_assoc 📋 Mathlib.CategoryTheory.Monoidal.Mod
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M : C) [CategoryTheory.AddMonObj M] (X : C) [CategoryTheory.AddModObj M X] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.AddMonObj.add X) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddModObj.vadd h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M M X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M CategoryTheory.AddModObj.vadd) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddModObj.vadd h)) - CategoryTheory.AddModObj.add_vadd_self_flip_assoc 📋 Mathlib.CategoryTheory.Monoidal.Mod
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : C} [CategoryTheory.AddMonObj M] (X : C) [CategoryTheory.AddModObj M X] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M CategoryTheory.AddModObj.vadd) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddModObj.vadd h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M M X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.AddMonObj.add X) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddModObj.vadd h)) - CategoryTheory.AddModObj.add_vadd 📋 Mathlib.CategoryTheory.Monoidal.Mod
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {D : Type u₂} {inst✝² : CategoryTheory.Category.{v₂, u₂} D} {inst✝³ : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D} {M : C} {inst✝⁴ : CategoryTheory.AddMonObj M} (X : D) [self : CategoryTheory.AddModObj M X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft CategoryTheory.AddMonObj.add X) CategoryTheory.AddModObj.vadd = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso M M X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight M CategoryTheory.AddModObj.vadd) CategoryTheory.AddModObj.vadd) - CategoryTheory.AddModObj.assoc_flip 📋 Mathlib.CategoryTheory.Monoidal.Mod
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {M : C} [CategoryTheory.AddMonObj M] (X : D) [CategoryTheory.AddModObj M X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight M CategoryTheory.AddModObj.vadd) CategoryTheory.AddModObj.vadd = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso M M X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft CategoryTheory.AddMonObj.add X) CategoryTheory.AddModObj.vadd) - CategoryTheory.AddModObj.add_vadd_assoc 📋 Mathlib.CategoryTheory.Monoidal.Mod
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {D : Type u₂} {inst✝² : CategoryTheory.Category.{v₂, u₂} D} {inst✝³ : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D} {M : C} {inst✝⁴ : CategoryTheory.AddMonObj M} (X : D) [self : CategoryTheory.AddModObj M X] {Z : D} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft CategoryTheory.AddMonObj.add X) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddModObj.vadd h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso M M X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight M CategoryTheory.AddModObj.vadd) (CategoryTheory.CategoryStruct.comp CategoryTheory.AddModObj.vadd h)) - CategoryTheory.AddModObj.mk 📋 Mathlib.CategoryTheory.Monoidal.Mod
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {M : C} [CategoryTheory.AddMonObj M] {X : D} (vadd : CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj M X ⟶ X) (zero_vadd : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft CategoryTheory.AddMonObj.zero X) vadd = (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X).hom := by cat_disch) (add_vadd : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft CategoryTheory.AddMonObj.add X) vadd = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso M M X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight M vadd) vadd) := by cat_disch) : CategoryTheory.AddModObj M X - CategoryTheory.AddMod.assoc_flip 📋 Mathlib.CategoryTheory.Monoidal.Mod
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {A : C} [CategoryTheory.AddMonObj A] (M : CategoryTheory.AddMod D A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A CategoryTheory.AddModObj.vadd) CategoryTheory.AddModObj.vadd = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso A A M.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft CategoryTheory.AddMonObj.add M.X) CategoryTheory.AddModObj.vadd) - CategoryTheory.RingObj.add_mul 📋 Mathlib.CategoryTheory.Monoidal.Ring
{C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.CartesianMonoidalCategory C} {inst✝² : CategoryTheory.BraidedCategory C} (R : C) [self : CategoryTheory.RingObj R] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.AddMonObj.add R) CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.SemiCartesianMonoidalCategory.fst R R) R) CategoryTheory.MonObj.mul) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.SemiCartesianMonoidalCategory.snd R R) R) CategoryTheory.MonObj.mul)) CategoryTheory.AddMonObj.add - CategoryTheory.RingObj.mul_add 📋 Mathlib.CategoryTheory.Monoidal.Ring
{C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.CartesianMonoidalCategory C} {inst✝² : 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 - CategoryTheory.add_mul_iff 📋 Mathlib.CategoryTheory.Monoidal.Ring
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (R : C) [CategoryTheory.MonObj R] [CategoryTheory.AddMonObj R] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.AddMonObj.add R) CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.SemiCartesianMonoidalCategory.fst R R) R) CategoryTheory.MonObj.mul) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.SemiCartesianMonoidalCategory.snd R R) R) CategoryTheory.MonObj.mul)) CategoryTheory.AddMonObj.add ↔ ∀ ⦃X : C⦄ (a b c : X ⟶ R), (a + b) * c = a * c + b * c - CategoryTheory.mul_add_iff 📋 Mathlib.CategoryTheory.Monoidal.Ring
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (R : C) [CategoryTheory.MonObj R] [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 - CategoryTheory.RingObj.mk 📋 Mathlib.CategoryTheory.Monoidal.Ring
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {R : C} [toAddGrpObj : CategoryTheory.AddGrpObj R] [toIsCommAddMonObj : CategoryTheory.IsCommAddMonObj R] [toMonObj : CategoryTheory.MonObj R] (mul_add : 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) (add_mul : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.AddMonObj.add R) CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.SemiCartesianMonoidalCategory.fst R R) R) CategoryTheory.MonObj.mul) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.SemiCartesianMonoidalCategory.snd R R) R) CategoryTheory.MonObj.mul)) CategoryTheory.AddMonObj.add) : CategoryTheory.RingObj R
About
Loogle searches Lean and Mathlib definitions and theorems.
You can use Loogle from within the Lean4 VSCode language extension
using the Loogle command from the command palette. You can also try the
#loogle command from LeanSearchClient,
the CLI version, the Loogle
VS Code extension, the lean.nvim
integration or the Zulip bot.
Usage
Loogle finds definitions and lemmas in various ways:
By constant:
🔍Real.sin
finds all lemmas whose statement somehow mentions the sine function.By lemma name substring:
🔍"differ"
finds all lemmas that have"differ"somewhere in their lemma name.By subexpression:
🔍_ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.The pattern can also be non-linear, as in
🔍Real.sqrt ?a * Real.sqrt ?aIf the pattern has parameters, they are matched in any order. Both of these will find
List.map:
🔍(?a -> ?b) -> List ?a -> List ?b
🔍List ?a -> (?a -> ?b) -> List ?bBy main conclusion:
🔍|- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all→and∀) has the given shape.As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍|- _ < _ → tsum _ < tsum _
will findtsum_lt_tsumeven though the hypothesisf i < g iis not the last.You can filter for definitions vs theorems: Using
⊢ (_ : Type _)finds all definitions which provide data while⊢ (_ : Prop)finds all theorems (and definitions of proofs).
If you pass more than one such search filter, separated by commas
Loogle will return lemmas which match all of them. The
search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin
and tsum, have "two" as a substring of the
lemma name, include a product and a power somewhere in the type,
and have a hypothesis of the form _ < _ (if
there were any such lemmas). Metavariables (?a) are
assigned independently in each filter.
The #lucky button will directly send you to the
documentation of the first hit.
Source code
You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.
This is Loogle revision 9f11169 serving mathlib revision ce5dd8c