Loogle!

Result

Found 93 declarations mentioning CategoryTheory.MonoidalPreadditive.

• CategoryTheory.MonoidalPreadditive 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] : Prop
• CategoryTheory.tensorLeft_additive 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (X : C) : (CategoryTheory.MonoidalCategory.tensorLeft X).Additive
• CategoryTheory.tensorRight_additive 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (X : C) : (CategoryTheory.MonoidalCategory.tensorRight X).Additive
• CategoryTheory.MonoidalPreadditive.instAdditiveTensorLeft 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (X : C) : (CategoryTheory.MonoidalCategory.tensorLeft X).Additive
• CategoryTheory.MonoidalPreadditive.instAdditiveTensorRight 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (X : C) : (CategoryTheory.MonoidalCategory.tensorRight X).Additive
• CategoryTheory.MonoidalPreadditive.instAdditiveFunctorCurriedTensor 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] : (CategoryTheory.MonoidalCategory.curriedTensor C).Additive
• CategoryTheory.tensoringLeft_additive 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (X : C) : ((CategoryTheory.MonoidalCategory.tensoringLeft C).obj X).Additive
• CategoryTheory.tensoringRight_additive 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (X : C) : ((CategoryTheory.MonoidalCategory.tensoringRight C).obj X).Additive
• CategoryTheory.MonoidalPreadditive.instAdditiveFunctorFlipCurriedTensor 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] : (CategoryTheory.MonoidalCategory.curriedTensor C).flip.Additive
• CategoryTheory.instPreservesFiniteBiproductsTensorLeft 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (X : C) : CategoryTheory.Limits.PreservesFiniteBiproducts (CategoryTheory.MonoidalCategory.tensorLeft X)
• CategoryTheory.monoidalPreadditive_of_faithful 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor D C) [F.Monoidal] [F.Faithful] [F.Additive] : CategoryTheory.MonoidalPreadditive D
• CategoryTheory.instPreservesFiniteBiproductsTensorRight 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (X : C) : CategoryTheory.Limits.PreservesFiniteBiproducts (CategoryTheory.MonoidalCategory.tensorRight X)
• CategoryTheory.leftDistributor 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (X : C) (f : J → C) : CategoryTheory.MonoidalCategoryStruct.tensorObj X (⨁ f) ≅ ⨁ fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j)
• CategoryTheory.rightDistributor 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (f : J → C) (X : C) : CategoryTheory.MonoidalCategoryStruct.tensorObj (⨁ f) X ≅ ⨁ fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X
• CategoryTheory.MonoidalPreadditive.whiskerLeft_zero 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} {inst✝ : CategoryTheory.Category.{v_1, u_1} C} {inst✝¹ : CategoryTheory.Preadditive C} {inst✝² : CategoryTheory.MonoidalCategory C} [self : CategoryTheory.MonoidalPreadditive C] {X Y Z : C} : CategoryTheory.MonoidalCategoryStruct.whiskerLeft X 0 = 0
• CategoryTheory.MonoidalPreadditive.zero_whiskerRight 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} {inst✝ : CategoryTheory.Category.{v_1, u_1} C} {inst✝¹ : CategoryTheory.Preadditive C} {inst✝² : CategoryTheory.MonoidalCategory C} [self : CategoryTheory.MonoidalPreadditive C] {X Y Z : C} : CategoryTheory.MonoidalCategoryStruct.whiskerRight 0 X = 0
• CategoryTheory.MonoidalPreadditive.tensor_zero 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {W X Y Z : C} (f : W ⟶ X) : CategoryTheory.MonoidalCategoryStruct.tensorHom f 0 = 0
• CategoryTheory.MonoidalPreadditive.zero_tensor 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {W X Y Z : C} (f : Y ⟶ Z) : CategoryTheory.MonoidalCategoryStruct.tensorHom 0 f = 0
• CategoryTheory.sum_whiskerRight 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {Q R : C} {J : Type u_2} (s : Finset J) (g : J → (Q ⟶ R)) (P : C) : CategoryTheory.MonoidalCategoryStruct.whiskerRight (∑ j ∈ s, g j) P = ∑ j ∈ s, CategoryTheory.MonoidalCategoryStruct.whiskerRight (g j) P
• CategoryTheory.whiskerLeft_sum 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (P : C) {Q R : C} {J : Type u_2} (s : Finset J) (g : J → (Q ⟶ R)) : CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (∑ j ∈ s, g j) = ∑ j ∈ s, CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (g j)
• CategoryTheory.sum_tensor 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {P Q R S : C} {J : Type u_2} (s : Finset J) (f : P ⟶ Q) (g : J → (R ⟶ S)) : CategoryTheory.MonoidalCategoryStruct.tensorHom (∑ j ∈ s, g j) f = ∑ j ∈ s, CategoryTheory.MonoidalCategoryStruct.tensorHom (g j) f
• CategoryTheory.tensor_sum 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {P Q R S : C} {J : Type u_2} (s : Finset J) (f : P ⟶ Q) (g : J → (R ⟶ S)) : CategoryTheory.MonoidalCategoryStruct.tensorHom f (∑ j ∈ s, g j) = ∑ j ∈ s, CategoryTheory.MonoidalCategoryStruct.tensorHom f (g j)
• CategoryTheory.biproduct_ι_comp_leftDistributor_inv 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (X : C) (f : J → C) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j)) j) (CategoryTheory.leftDistributor X f).inv = CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.ι f j)
• CategoryTheory.biproduct_ι_comp_rightDistributor_inv 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (f : J → C) (X : C) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X) j) (CategoryTheory.rightDistributor f X).inv = CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X
• CategoryTheory.leftDistributor_hom_comp_biproduct_π 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (X : C) (f : J → C) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.leftDistributor X f).hom (CategoryTheory.Limits.biproduct.π (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j)) j) = CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.π f j)
• CategoryTheory.rightDistributor_hom_comp_biproduct_π 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (f : J → C) (X : C) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.rightDistributor f X).hom (CategoryTheory.Limits.biproduct.π (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X) j) = CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.π f j) X
• CategoryTheory.biproduct_ι_comp_leftDistributor_hom 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (X : C) (f : J → C) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.ι f j)) (CategoryTheory.leftDistributor X f).hom = CategoryTheory.Limits.biproduct.ι (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j)) j
• CategoryTheory.biproduct_ι_comp_rightDistributor_hom 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (f : J → C) (X : C) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X) (CategoryTheory.rightDistributor f X).hom = CategoryTheory.Limits.biproduct.ι (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X) j
• CategoryTheory.leftDistributor_inv_comp_biproduct_π 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (X : C) (f : J → C) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.leftDistributor X f).inv (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.π f j)) = CategoryTheory.Limits.biproduct.π (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j)) j
• CategoryTheory.rightDistributor_inv_comp_biproduct_π 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (f : J → C) (X : C) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.rightDistributor f X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.π f j) X) = CategoryTheory.Limits.biproduct.π (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X) j
• CategoryTheory.MonoidalPreadditive.add_whiskerRight 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} {inst✝ : CategoryTheory.Category.{v_1, u_1} C} {inst✝¹ : CategoryTheory.Preadditive C} {inst✝² : CategoryTheory.MonoidalCategory C} [self : CategoryTheory.MonoidalPreadditive C] {X Y Z : C} (f g : Y ⟶ Z) : CategoryTheory.MonoidalCategoryStruct.whiskerRight (f + g) X = CategoryTheory.MonoidalCategoryStruct.whiskerRight f X + CategoryTheory.MonoidalCategoryStruct.whiskerRight g X
• CategoryTheory.MonoidalPreadditive.whiskerLeft_add 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} {inst✝ : CategoryTheory.Category.{v_1, u_1} C} {inst✝¹ : CategoryTheory.Preadditive C} {inst✝² : CategoryTheory.MonoidalCategory C} [self : CategoryTheory.MonoidalPreadditive C] {X Y Z : C} (f g : Y ⟶ Z) : CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (f + g) = CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f + CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g
• CategoryTheory.leftDistributor_ext_left 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {X Y : C} {f : J → C} {g h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (⨁ f) ⟶ Y} (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.ι f j)) g = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.ι f j)) h) : g = h
• CategoryTheory.leftDistributor_ext_right 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {X Y : C} {f : J → C} {g h : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Y (⨁ f)} (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp g (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (CategoryTheory.Limits.biproduct.π f j)) = CategoryTheory.CategoryStruct.comp h (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (CategoryTheory.Limits.biproduct.π f j))) : g = h
• CategoryTheory.rightDistributor_ext_left 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {f : J → C} {X Y : C} {g h : CategoryTheory.MonoidalCategoryStruct.tensorObj (⨁ f) X ⟶ Y} (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X) g = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X) h) : g = h
• CategoryTheory.rightDistributor_ext_right 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {f : J → C} {X Y : C} {g h : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (⨁ f) Y} (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp g (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.π f j) Y) = CategoryTheory.CategoryStruct.comp h (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.π f j) Y)) : g = h
• CategoryTheory.MonoidalPreadditive.add_tensor 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {W X Y Z : C} (f g : W ⟶ X) (h : Y ⟶ Z) : CategoryTheory.MonoidalCategoryStruct.tensorHom (f + g) h = CategoryTheory.MonoidalCategoryStruct.tensorHom f h + CategoryTheory.MonoidalCategoryStruct.tensorHom g h
• CategoryTheory.MonoidalPreadditive.tensor_add 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {W X Y Z : C} (f : W ⟶ X) (g h : Y ⟶ Z) : CategoryTheory.MonoidalCategoryStruct.tensorHom f (g + h) = CategoryTheory.MonoidalCategoryStruct.tensorHom f g + CategoryTheory.MonoidalCategoryStruct.tensorHom f h
• CategoryTheory.leftDistributor_ext_left_iff 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {X Y : C} {f : J → C} {g h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (⨁ f) ⟶ Y} : g = h ↔ ∀ (j : J), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.ι f j)) g = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.ι f j)) h
• CategoryTheory.leftDistributor_ext_right_iff 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {X Y : C} {f : J → C} {g h : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Y (⨁ f)} : g = h ↔ ∀ (j : J), CategoryTheory.CategoryStruct.comp g (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (CategoryTheory.Limits.biproduct.π f j)) = CategoryTheory.CategoryStruct.comp h (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (CategoryTheory.Limits.biproduct.π f j))
• CategoryTheory.rightDistributor_ext_left_iff 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {f : J → C} {X Y : C} {g h : CategoryTheory.MonoidalCategoryStruct.tensorObj (⨁ f) X ⟶ Y} : g = h ↔ ∀ (j : J), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X) g = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X) h
• CategoryTheory.rightDistributor_ext_right_iff 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {f : J → C} {X Y : C} {g h : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (⨁ f) Y} : g = h ↔ ∀ (j : J), CategoryTheory.CategoryStruct.comp g (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.π f j) Y) = CategoryTheory.CategoryStruct.comp h (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.π f j) Y)
• CategoryTheory.biproduct_ι_comp_leftDistributor_inv_assoc 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (X : C) (f : J → C) (j : J) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (⨁ f) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j)) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.leftDistributor X f).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.ι f j)) h
• CategoryTheory.biproduct_ι_comp_rightDistributor_inv_assoc 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (f : J → C) (X : C) (j : J) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (⨁ f) X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.rightDistributor f X).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X) h
• CategoryTheory.leftDistributor_hom_comp_biproduct_π_assoc 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (X : C) (f : J → C) (j : J) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.leftDistributor X f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j)) j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.π f j)) h
• CategoryTheory.rightDistributor_hom_comp_biproduct_π_assoc 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (f : J → C) (X : C) (j : J) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.rightDistributor f X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X) j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.π f j) X) h
• CategoryTheory.biproduct_ι_comp_leftDistributor_hom_assoc 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (X : C) (f : J → C) (j : J) {Z : C} (h : (⨁ fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.ι f j)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.leftDistributor X f).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j)) j) h
• CategoryTheory.biproduct_ι_comp_rightDistributor_hom_assoc 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (f : J → C) (X : C) (j : J) {Z : C} (h : (⨁ fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.rightDistributor f X).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X) j) h
• CategoryTheory.leftDistributor_inv_comp_biproduct_π_assoc 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (X : C) (f : J → C) (j : J) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.leftDistributor X f).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.π f j)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j)) j) h
• CategoryTheory.rightDistributor_inv_comp_biproduct_π_assoc 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (f : J → C) (X : C) (j : J) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.rightDistributor f X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.π f j) X) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X) j) h
• CategoryTheory.leftDistributor_ext₂_left 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {X Y Z : C} {f : J → C} {g h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y (⨁ f)) ⟶ Z} (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (CategoryTheory.Limits.biproduct.ι f j))) g = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (CategoryTheory.Limits.biproduct.ι f j))) h) : g = h
• CategoryTheory.leftDistributor_ext₂_right 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {X Y Z : C} {f : J → C} {g h : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Y (CategoryTheory.MonoidalCategoryStruct.tensorObj Z (⨁ f))} (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp g (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z (CategoryTheory.Limits.biproduct.π f j))) = CategoryTheory.CategoryStruct.comp h (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z (CategoryTheory.Limits.biproduct.π f j)))) : g = h
• CategoryTheory.rightDistributor_ext₂_left 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {f : J → C} {X Y Z : C} {g h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj (⨁ f) X) Y ⟶ Z} (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X) Y) g = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X) Y) h) : g = h
• CategoryTheory.rightDistributor_ext₂_right 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {f : J → C} {X Y Z : C} {g h : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj (⨁ f) Y) Z} (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp g (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.π f j) Y) Z) = CategoryTheory.CategoryStruct.comp h (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.π f j) Y) Z)) : g = h
• CategoryTheory.leftDistributor_ext₂_left_iff 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {X Y Z : C} {f : J → C} {g h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y (⨁ f)) ⟶ Z} : g = h ↔ ∀ (j : J), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (CategoryTheory.Limits.biproduct.ι f j))) g = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (CategoryTheory.Limits.biproduct.ι f j))) h
• CategoryTheory.leftDistributor_ext₂_right_iff 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {X Y Z : C} {f : J → C} {g h : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Y (CategoryTheory.MonoidalCategoryStruct.tensorObj Z (⨁ f))} : g = h ↔ ∀ (j : J), CategoryTheory.CategoryStruct.comp g (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z (CategoryTheory.Limits.biproduct.π f j))) = CategoryTheory.CategoryStruct.comp h (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z (CategoryTheory.Limits.biproduct.π f j)))
• CategoryTheory.rightDistributor_ext₂_left_iff 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {f : J → C} {X Y Z : C} {g h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj (⨁ f) X) Y ⟶ Z} : g = h ↔ ∀ (j : J), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X) Y) g = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X) Y) h
• CategoryTheory.rightDistributor_ext₂_right_iff 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] {f : J → C} {X Y Z : C} {g h : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj (⨁ f) Y) Z} : g = h ↔ ∀ (j : J), CategoryTheory.CategoryStruct.comp g (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.π f j) Y) Z) = CategoryTheory.CategoryStruct.comp h (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.π f j) Y) Z)
• CategoryTheory.leftDistributor_hom 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Fintype J] (X : C) (f : J → C) : (CategoryTheory.leftDistributor X f).hom = ∑ j, CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.π f j)) (CategoryTheory.Limits.biproduct.ι (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j)) j)
• CategoryTheory.leftDistributor_inv 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Fintype J] (X : C) (f : J → C) : (CategoryTheory.leftDistributor X f).inv = ∑ j, CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j)) j) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.ι f j))
• CategoryTheory.rightDistributor_hom 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Fintype J] (f : J → C) (X : C) : (CategoryTheory.rightDistributor f X).hom = ∑ j, CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.π f j) X) (CategoryTheory.Limits.biproduct.ι (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X) j)
• CategoryTheory.rightDistributor_inv 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Fintype J] (f : J → C) (X : C) : (CategoryTheory.rightDistributor f X).inv = ∑ j, CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X) j) (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X)
• CategoryTheory.rightDistributor_assoc 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (f : J → C) (X Y : C) : CategoryTheory.MonoidalCategory.tensorIso (CategoryTheory.rightDistributor f X) (CategoryTheory.asIso (CategoryTheory.CategoryStruct.id Y)) ≪≫ CategoryTheory.rightDistributor (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X) Y = CategoryTheory.MonoidalCategoryStruct.associator (⨁ f) X Y ≪≫ CategoryTheory.rightDistributor f (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) ≪≫ CategoryTheory.Limits.biproduct.mapIso fun x => (CategoryTheory.MonoidalCategoryStruct.associator (f x) X Y).symm
• CategoryTheory.leftDistributor_assoc 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (X Y : C) (f : J → C) : (CategoryTheory.MonoidalCategory.tensorIso (CategoryTheory.asIso (CategoryTheory.CategoryStruct.id X)) (CategoryTheory.leftDistributor Y f) ≪≫ CategoryTheory.leftDistributor X fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj Y (f j)) = (CategoryTheory.MonoidalCategoryStruct.associator X Y (⨁ f)).symm ≪≫ CategoryTheory.leftDistributor (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) f ≪≫ CategoryTheory.Limits.biproduct.mapIso fun x => CategoryTheory.MonoidalCategoryStruct.associator X Y (f x)
• CategoryTheory.MonoidalPreadditive.mk 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] (whiskerLeft_zero : ∀ {X Y Z : C}, CategoryTheory.MonoidalCategoryStruct.whiskerLeft X 0 = 0 := by cat_disch) (zero_whiskerRight : ∀ {X Y Z : C}, CategoryTheory.MonoidalCategoryStruct.whiskerRight 0 X = 0 := by cat_disch) (whiskerLeft_add : ∀ {X Y Z : C} (f g : Y ⟶ Z), CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (f + g) = CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f + CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g := by cat_disch) (add_whiskerRight : ∀ {X Y Z : C} (f g : Y ⟶ Z), CategoryTheory.MonoidalCategoryStruct.whiskerRight (f + g) X = CategoryTheory.MonoidalCategoryStruct.whiskerRight f X + CategoryTheory.MonoidalCategoryStruct.whiskerRight g X := by cat_disch) : CategoryTheory.MonoidalPreadditive C
• CategoryTheory.leftDistributor_rightDistributor_assoc 📋 Mathlib.CategoryTheory.Monoidal.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (X : C) (f : J → C) (Y : C) : CategoryTheory.MonoidalCategory.tensorIso (CategoryTheory.leftDistributor X f) (CategoryTheory.asIso (CategoryTheory.CategoryStruct.id Y)) ≪≫ CategoryTheory.rightDistributor (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j)) Y = CategoryTheory.MonoidalCategoryStruct.associator X (⨁ f) Y ≪≫ CategoryTheory.MonoidalCategory.tensorIso (CategoryTheory.asIso (CategoryTheory.CategoryStruct.id X)) (CategoryTheory.rightDistributor f Y) ≪≫ (CategoryTheory.leftDistributor X fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) Y) ≪≫ CategoryTheory.Limits.biproduct.mapIso fun x => (CategoryTheory.MonoidalCategoryStruct.associator X (f x) Y).symm
• CategoryTheory.MonoidalLinear 📋 Mathlib.CategoryTheory.Monoidal.Linear
  (R : Type u_1) [Semiring R] (C : Type u_2) [CategoryTheory.Category.{v_1, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] : Prop
• CategoryTheory.tensorLeft_linear 📋 Mathlib.CategoryTheory.Monoidal.Linear
  (R : Type u_1) [Semiring R] {C : Type u_2} [CategoryTheory.Category.{v_1, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.MonoidalLinear R C] (X : C) : CategoryTheory.Functor.Linear R (CategoryTheory.MonoidalCategory.tensorLeft X)
• CategoryTheory.tensorRight_linear 📋 Mathlib.CategoryTheory.Monoidal.Linear
  (R : Type u_1) [Semiring R] {C : Type u_2} [CategoryTheory.Category.{v_1, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.MonoidalLinear R C] (X : C) : CategoryTheory.Functor.Linear R (CategoryTheory.MonoidalCategory.tensorRight X)
• CategoryTheory.tensoringLeft_linear 📋 Mathlib.CategoryTheory.Monoidal.Linear
  (R : Type u_1) [Semiring R] {C : Type u_2} [CategoryTheory.Category.{v_1, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.MonoidalLinear R C] (X : C) : CategoryTheory.Functor.Linear R ((CategoryTheory.MonoidalCategory.tensoringLeft C).obj X)
• CategoryTheory.tensoringRight_linear 📋 Mathlib.CategoryTheory.Monoidal.Linear
  (R : Type u_1) [Semiring R] {C : Type u_2} [CategoryTheory.Category.{v_1, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.MonoidalLinear R C] (X : C) : CategoryTheory.Functor.Linear R ((CategoryTheory.MonoidalCategory.tensoringRight C).obj X)
• CategoryTheory.MonoidalLinear.ofFaithful 📋 Mathlib.CategoryTheory.Monoidal.Linear
  (R : Type u_1) [Semiring R] {C : Type u_2} [CategoryTheory.Category.{v_1, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.MonoidalLinear R C] {D : Type u_3} [CategoryTheory.Category.{v_2, u_3} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear R D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.MonoidalPreadditive D] (F : CategoryTheory.Functor D C) [F.Monoidal] [F.Faithful] [CategoryTheory.Functor.Linear R F] : CategoryTheory.MonoidalLinear R D
• CategoryTheory.MonoidalLinear.smul_whiskerRight 📋 Mathlib.CategoryTheory.Monoidal.Linear
  {R : Type u_1} {inst✝ : Semiring R} {C : Type u_2} {inst✝¹ : CategoryTheory.Category.{v_1, u_2} C} {inst✝² : CategoryTheory.Preadditive C} {inst✝³ : CategoryTheory.Linear R C} {inst✝⁴ : CategoryTheory.MonoidalCategory C} {inst✝⁵ : 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
• CategoryTheory.MonoidalLinear.whiskerLeft_smul 📋 Mathlib.CategoryTheory.Monoidal.Linear
  {R : Type u_1} {inst✝ : Semiring R} {C : Type u_2} {inst✝¹ : CategoryTheory.Category.{v_1, u_2} C} {inst✝² : CategoryTheory.Preadditive C} {inst✝³ : CategoryTheory.Linear R C} {inst✝⁴ : CategoryTheory.MonoidalCategory C} {inst✝⁵ : CategoryTheory.MonoidalPreadditive C} [self : CategoryTheory.MonoidalLinear R C] (X : C) {Y Z : C} (r : R) (f : Y ⟶ Z) : CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (r • f) = r • CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f
• CategoryTheory.MonoidalLinear.mk 📋 Mathlib.CategoryTheory.Monoidal.Linear
  {R : Type u_1} [Semiring R] {C : Type u_2} [CategoryTheory.Category.{v_1, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (whiskerLeft_smul : ∀ (X : C) {Y Z : C} (r : R) (f : Y ⟶ Z), CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (r • f) = r • CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f := by cat_disch) (smul_whiskerRight : ∀ (r : R) {Y Z : C} (f : Y ⟶ Z) (X : C), CategoryTheory.MonoidalCategoryStruct.whiskerRight (r • f) X = r • CategoryTheory.MonoidalCategoryStruct.whiskerRight f X := by cat_disch) : CategoryTheory.MonoidalLinear R C
• ModuleCat.instMonoidalPreadditive 📋 Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
  {R : Type u} [CommRing R] : CategoryTheory.MonoidalPreadditive (ModuleCat R)
• CategoryTheory.ObjectProperty.instMonoidalPreadditiveFullSubcategory 📋 Mathlib.CategoryTheory.Monoidal.Subcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : CategoryTheory.ObjectProperty C) [P.IsMonoidal] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] : CategoryTheory.MonoidalPreadditive P.FullSubcategory
• CategoryTheory.ObjectProperty.instMonoidalLinearFullSubcategory 📋 Mathlib.CategoryTheory.Monoidal.Subcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : CategoryTheory.ObjectProperty C) [P.IsMonoidal] [CategoryTheory.Preadditive C] (R : Type u_1) [Ring R] [CategoryTheory.Linear R C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.MonoidalLinear R C] : CategoryTheory.MonoidalLinear R P.FullSubcategory
• Action.instMonoidalPreadditive 📋 Mathlib.CategoryTheory.Action.Monoidal
  (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [Monoid G] [CategoryTheory.MonoidalCategory V] [CategoryTheory.Preadditive V] [CategoryTheory.MonoidalPreadditive V] : CategoryTheory.MonoidalPreadditive (Action V G)
• Action.instMonoidalLinear 📋 Mathlib.CategoryTheory.Action.Monoidal
  (V : Type u_1) [CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [Monoid G] [CategoryTheory.MonoidalCategory V] [CategoryTheory.Preadditive V] [CategoryTheory.MonoidalPreadditive V] {R : Type u_3} [Semiring R] [CategoryTheory.Linear R V] [CategoryTheory.MonoidalLinear R V] : CategoryTheory.MonoidalLinear R (Action V G)
• CategoryTheory.IsMonoidalDistrib.of_MonoidalPreadditive_with_binary_coproducts 📋 Mathlib.CategoryTheory.Distributive.Monoidal
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] : CategoryTheory.IsMonoidalDistrib C
• CategoryTheory.Limits.CokernelCofork.tensor 📋 Mathlib.CategoryTheory.Monoidal.Limits.Cokernels
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {X₁ Y₁ : C} {f₁ : X₁ ⟶ Y₁} (c₁ : CategoryTheory.Limits.CokernelCofork f₁) {X₂ Y₂ : C} {f₂ : X₂ ⟶ Y₂} (c₂ : CategoryTheory.Limits.CokernelCofork f₂) [CategoryTheory.Limits.HasBinaryCoproduct (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ Y₂) (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₁ X₂)] : CategoryTheory.Limits.CokernelCofork (CategoryTheory.Limits.coprod.desc (CategoryTheory.MonoidalCategoryStruct.whiskerRight f₁ Y₂) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y₁ f₂))
• CategoryTheory.Limits.CokernelCofork.isColimitTensor 📋 Mathlib.CategoryTheory.Monoidal.Limits.Cokernels
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {X₁ Y₁ : C} {f₁ : X₁ ⟶ Y₁} {c₁ : CategoryTheory.Limits.CokernelCofork f₁} (hc₁ : CategoryTheory.Limits.IsColimit c₁) {X₂ Y₂ : C} {f₂ : X₂ ⟶ Y₂} {c₂ : CategoryTheory.Limits.CokernelCofork f₂} (hc₂ : CategoryTheory.Limits.IsColimit c₂) [CategoryTheory.Limits.HasBinaryCoproduct (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ Y₂) (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₁ X₂)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f₂ 0) (CategoryTheory.MonoidalCategory.tensorLeft c₁.pt)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f₁ 0) (CategoryTheory.MonoidalCategory.tensorRight Y₂)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f₁ 0) (CategoryTheory.MonoidalCategory.tensorRight X₂)] : CategoryTheory.Limits.IsColimit (c₁.tensor c₂)
• CategoryTheory.Tor 📋 Mathlib.CategoryTheory.Monoidal.Tor
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.HasProjectiveResolutions C] (n : ℕ) : CategoryTheory.Functor C (CategoryTheory.Functor C C)
• CategoryTheory.Tor' 📋 Mathlib.CategoryTheory.Monoidal.Tor
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.HasProjectiveResolutions C] (n : ℕ) : CategoryTheory.Functor C (CategoryTheory.Functor C C)
• CategoryTheory.isZero_Tor'_succ_of_projective 📋 Mathlib.CategoryTheory.Monoidal.Tor
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.HasProjectiveResolutions C] (X Y : C) [CategoryTheory.Projective X] (n : ℕ) : CategoryTheory.Limits.IsZero (((CategoryTheory.Tor' C (n + 1)).obj X).obj Y)
• CategoryTheory.isZero_Tor_succ_of_projective 📋 Mathlib.CategoryTheory.Monoidal.Tor
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.HasProjectiveResolutions C] (X Y : C) [CategoryTheory.Projective Y] (n : ℕ) : CategoryTheory.Limits.IsZero (((CategoryTheory.Tor C (n + 1)).obj X).obj Y)
• CategoryTheory.Tor_obj 📋 Mathlib.CategoryTheory.Monoidal.Tor
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.HasProjectiveResolutions C] (n : ℕ) (X : C) : (CategoryTheory.Tor C n).obj X = ((CategoryTheory.MonoidalCategory.tensoringLeft C).obj X).leftDerived n
• CategoryTheory.Tor'_obj_obj 📋 Mathlib.CategoryTheory.Monoidal.Tor
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.HasProjectiveResolutions C] (n : ℕ) (k j : C) : ((CategoryTheory.Tor' C n).obj k).obj j = (((CategoryTheory.MonoidalCategory.tensoringRight C).obj j).leftDerived n).obj k
• CategoryTheory.Tor_map 📋 Mathlib.CategoryTheory.Monoidal.Tor
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.HasProjectiveResolutions C] (n : ℕ) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (CategoryTheory.Tor C n).map f = CategoryTheory.NatTrans.leftDerived ((CategoryTheory.MonoidalCategory.tensoringLeft C).map f) n
• CategoryTheory.Tor'_obj_map 📋 Mathlib.CategoryTheory.Monoidal.Tor
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.HasProjectiveResolutions C] (n : ℕ) (k : C) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Tor' C n).obj k).map f = (CategoryTheory.NatTrans.leftDerived ((CategoryTheory.MonoidalCategory.tensoringRight C).map f) n).app k
• CategoryTheory.Tor'_map_app 📋 Mathlib.CategoryTheory.Monoidal.Tor
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.HasProjectiveResolutions C] (n : ℕ) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (j : C) : ((CategoryTheory.Tor' C n).map f).app j = (((CategoryTheory.MonoidalCategory.tensoringRight C).obj j).leftDerived n).map f
• Rep.instMonoidalPreadditive 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [CommRing k] [Monoid G] : CategoryTheory.MonoidalPreadditive (Rep.{u, u, v} k G)

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:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. 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 ?a

   If 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 ?b

4. By 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 find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. 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