Loogle!

Result

Found 84 declarations mentioning CategoryTheory.DifferentialObject.

• CategoryTheory.DifferentialObject 📋 Mathlib.CategoryTheory.DifferentialObject
  (S : Type u_1) [AddMonoidWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] : Type (max u v)
• CategoryTheory.DifferentialObject.categoryOfDifferentialObjects 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] : CategoryTheory.Category.{v, max u v} (CategoryTheory.DifferentialObject S C)
• CategoryTheory.DifferentialObject.obj 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (self : CategoryTheory.DifferentialObject S C) : C
• CategoryTheory.DifferentialObject.Hom 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (X Y : CategoryTheory.DifferentialObject S C) : Type v
• CategoryTheory.DifferentialObject.Hom.id 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (X : CategoryTheory.DifferentialObject S C) : X.Hom X
• CategoryTheory.DifferentialObject.forget 📋 Mathlib.CategoryTheory.DifferentialObject
  (S : Type u_1) [AddMonoidWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] : CategoryTheory.Functor (CategoryTheory.DifferentialObject S C) C
• CategoryTheory.DifferentialObject.forget_faithful 📋 Mathlib.CategoryTheory.DifferentialObject
  (S : Type u_1) [AddMonoidWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] : (CategoryTheory.DifferentialObject.forget S C).Faithful
• CategoryTheory.DifferentialObject.instHasShift 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] : CategoryTheory.HasShift (CategoryTheory.DifferentialObject S C) S
• CategoryTheory.DifferentialObject.HomSubtype 📋 Mathlib.CategoryTheory.DifferentialObject
  (S : Type u_1) [AddMonoidWithOne S] (C : Type (u + 1)) [CategoryTheory.LargeCategory C] [CategoryTheory.Limits.HasZeroMorphisms C] {FC : C → C → Type u_2} {CC : C → Type u_3} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.HasShift C S] (X Y : CategoryTheory.DifferentialObject S C) : Type u_2
• CategoryTheory.DifferentialObject.hasZeroMorphisms 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] [(CategoryTheory.shiftFunctor C 1).PreservesZeroMorphisms] : CategoryTheory.Limits.HasZeroMorphisms (CategoryTheory.DifferentialObject S C)
• CategoryTheory.DifferentialObject.hasZeroObject 📋 Mathlib.CategoryTheory.DifferentialObject
  (S : Type u_1) [AddMonoidWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] [(CategoryTheory.shiftFunctor C 1).PreservesZeroMorphisms] : CategoryTheory.Limits.HasZeroObject (CategoryTheory.DifferentialObject S C)
• CategoryTheory.DifferentialObject.Hom.f 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (self : X.Hom Y) : X.obj ⟶ Y.obj
• CategoryTheory.DifferentialObject.Hom.comp 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y Z : CategoryTheory.DifferentialObject S C} (f : X.Hom Y) (g : Y.Hom Z) : X.Hom Z
• CategoryTheory.DifferentialObject.isoApp 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (f : X ≅ Y) : X.obj ≅ Y.obj
• CategoryTheory.DifferentialObject.shiftFunctor 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (n : S) : CategoryTheory.Functor (CategoryTheory.DifferentialObject S C) (CategoryTheory.DifferentialObject S C)
• CategoryTheory.DifferentialObject.d 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (self : CategoryTheory.DifferentialObject S C) : self.obj ⟶ (CategoryTheory.shiftFunctor C 1).obj self.obj
• CategoryTheory.DifferentialObject.Hom.id_f 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (X : CategoryTheory.DifferentialObject S C) : (CategoryTheory.DifferentialObject.Hom.id X).f = CategoryTheory.CategoryStruct.id X.obj
• CategoryTheory.DifferentialObject.isoApp_refl 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (X : CategoryTheory.DifferentialObject S C) : CategoryTheory.DifferentialObject.isoApp (CategoryTheory.Iso.refl X) = CategoryTheory.Iso.refl X.obj
• CategoryTheory.DifferentialObject.instFunLikeHomSubtypeObj 📋 Mathlib.CategoryTheory.DifferentialObject
  (S : Type u_1) [AddMonoidWithOne S] (C : Type (u + 1)) [CategoryTheory.LargeCategory C] [CategoryTheory.Limits.HasZeroMorphisms C] {FC : C → C → Type u_2} {CC : C → Type u_3} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.HasShift C S] (X Y : CategoryTheory.DifferentialObject S C) : FunLike (CategoryTheory.DifferentialObject.HomSubtype S C X Y) (CC X.obj) (CC Y.obj)
• CategoryTheory.DifferentialObject.instZeroHom 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] [(CategoryTheory.shiftFunctor C 1).PreservesZeroMorphisms] {X Y : CategoryTheory.DifferentialObject S C} : Zero (X ⟶ Y)
• CategoryTheory.DifferentialObject.concreteCategoryOfDifferentialObjects 📋 Mathlib.CategoryTheory.DifferentialObject
  (S : Type u_1) [AddMonoidWithOne S] (C : Type (u + 1)) [CategoryTheory.LargeCategory C] [CategoryTheory.Limits.HasZeroMorphisms C] {FC : C → C → Type u_2} {CC : C → Type u_3} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.HasShift C S] : CategoryTheory.ConcreteCategory (CategoryTheory.DifferentialObject S C) (CategoryTheory.DifferentialObject.HomSubtype S C)
• CategoryTheory.DifferentialObject.id_f 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (X : CategoryTheory.DifferentialObject S C) : (CategoryTheory.CategoryStruct.id X).f = CategoryTheory.CategoryStruct.id X.obj
• CategoryTheory.DifferentialObject.Hom.ext 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} {inst✝ : AddMonoidWithOne S} {C : Type u} {inst✝¹ : CategoryTheory.Category.{v, u} C} {inst✝² : CategoryTheory.Limits.HasZeroMorphisms C} {inst✝³ : CategoryTheory.HasShift C S} {X Y : CategoryTheory.DifferentialObject S C} {x y : X.Hom Y} (f : x.f = y.f) : x = y
• CategoryTheory.DifferentialObject.Hom.ext_iff 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} {inst✝ : AddMonoidWithOne S} {C : Type u} {inst✝¹ : CategoryTheory.Category.{v, u} C} {inst✝² : CategoryTheory.Limits.HasZeroMorphisms C} {inst✝³ : CategoryTheory.HasShift C S} {X Y : CategoryTheory.DifferentialObject S C} {x y : X.Hom Y} : x = y ↔ x.f = y.f
• CategoryTheory.DifferentialObject.instHasForget₂HomSubtypeObj 📋 Mathlib.CategoryTheory.DifferentialObject
  (S : Type u_1) [AddMonoidWithOne S] (C : Type (u + 1)) [CategoryTheory.LargeCategory C] [CategoryTheory.Limits.HasZeroMorphisms C] {FC : C → C → Type u_2} {CC : C → Type u_3} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.HasShift C S] : CategoryTheory.HasForget₂ (CategoryTheory.DifferentialObject S C) C
• CategoryTheory.DifferentialObject.isoApp_symm 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (f : X ≅ Y) : CategoryTheory.DifferentialObject.isoApp f.symm = (CategoryTheory.DifferentialObject.isoApp f).symm
• CategoryTheory.DifferentialObject.isoApp_hom 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (f : X ≅ Y) : (CategoryTheory.DifferentialObject.isoApp f).hom = f.hom.f
• CategoryTheory.DifferentialObject.isoApp_inv 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (f : X ≅ Y) : (CategoryTheory.DifferentialObject.isoApp f).inv = f.inv.f
• CategoryTheory.DifferentialObject.shiftFunctor_obj_obj 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (n : S) (X : CategoryTheory.DifferentialObject S C) : ((CategoryTheory.DifferentialObject.shiftFunctor C n).obj X).obj = (CategoryTheory.shiftFunctor C n).obj X.obj
• CategoryTheory.DifferentialObject.eqToHom_f 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (h : X = Y) : (CategoryTheory.eqToHom h).f = CategoryTheory.eqToHom ⋯
• CategoryTheory.DifferentialObject.Hom.comp_f 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y Z : CategoryTheory.DifferentialObject S C} (f : X.Hom Y) (g : Y.Hom Z) : (f.comp g).f = CategoryTheory.CategoryStruct.comp f.f g.f
• CategoryTheory.DifferentialObject.shiftZero 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] : CategoryTheory.DifferentialObject.shiftFunctor C 0 ≅ CategoryTheory.Functor.id (CategoryTheory.DifferentialObject S C)
• CategoryTheory.DifferentialObject.isoApp_trans 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y Z : CategoryTheory.DifferentialObject S C} (f : X ≅ Y) (g : Y ≅ Z) : CategoryTheory.DifferentialObject.isoApp (f ≪≫ g) = CategoryTheory.DifferentialObject.isoApp f ≪≫ CategoryTheory.DifferentialObject.isoApp g
• CategoryTheory.DifferentialObject.ext 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {A B : CategoryTheory.DifferentialObject S C} {f g : A ⟶ B} (w : f.f = g.f := by cat_disch) : f = g
• CategoryTheory.DifferentialObject.ext_iff 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {A B : CategoryTheory.DifferentialObject S C} {f g : A ⟶ B} : f = g ↔ autoParam (f.f = g.f) CategoryTheory.DifferentialObject.ext._auto_1
• CategoryTheory.DifferentialObject.comp_f 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y Z : CategoryTheory.DifferentialObject S C} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).f = CategoryTheory.CategoryStruct.comp f.f g.f
• CategoryTheory.DifferentialObject.shiftFunctorAdd 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (m n : S) : CategoryTheory.DifferentialObject.shiftFunctor C (m + n) ≅ (CategoryTheory.DifferentialObject.shiftFunctor C m).comp (CategoryTheory.DifferentialObject.shiftFunctor C n)
• CategoryTheory.DifferentialObject.zero_f 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] [(CategoryTheory.shiftFunctor C 1).PreservesZeroMorphisms] (P Q : CategoryTheory.DifferentialObject S C) : CategoryTheory.DifferentialObject.Hom.f 0 = 0
• CategoryTheory.Functor.mapDifferentialObject 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (D : Type u') [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms D] [CategoryTheory.HasShift D S] (F : CategoryTheory.Functor C D) (η : (CategoryTheory.shiftFunctor C 1).comp F ⟶ F.comp (CategoryTheory.shiftFunctor D 1)) (hF : ∀ (c c' : C), F.map 0 = 0) : CategoryTheory.Functor (CategoryTheory.DifferentialObject S C) (CategoryTheory.DifferentialObject S D)
• CategoryTheory.DifferentialObject.Hom.comm 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (self : X.Hom Y) : CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map self.f) = CategoryTheory.CategoryStruct.comp self.f Y.d
• CategoryTheory.DifferentialObject.Hom.mk 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (f : X.obj ⟶ Y.obj) (comm : CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f) = CategoryTheory.CategoryStruct.comp f Y.d := by cat_disch) : X.Hom Y
• CategoryTheory.Functor.mapDifferentialObject_obj_obj 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (D : Type u') [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms D] [CategoryTheory.HasShift D S] (F : CategoryTheory.Functor C D) (η : (CategoryTheory.shiftFunctor C 1).comp F ⟶ F.comp (CategoryTheory.shiftFunctor D 1)) (hF : ∀ (c c' : C), F.map 0 = 0) (X : CategoryTheory.DifferentialObject S C) : ((CategoryTheory.Functor.mapDifferentialObject D F η hF).obj X).obj = F.obj X.obj
• CategoryTheory.DifferentialObject.mkIso 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (f : X.obj ≅ Y.obj) (hf : CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f.hom) = CategoryTheory.CategoryStruct.comp f.hom Y.d) : X ≅ Y
• CategoryTheory.DifferentialObject.Hom.comm_assoc 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (self : X.Hom Y) {Z : C} (h : (CategoryTheory.shiftFunctor C 1).obj Y.obj ⟶ Z) : CategoryTheory.CategoryStruct.comp X.d (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C 1).map self.f) h) = CategoryTheory.CategoryStruct.comp self.f (CategoryTheory.CategoryStruct.comp Y.d h)
• CategoryTheory.DifferentialObject.mk 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (obj : C) (d : obj ⟶ (CategoryTheory.shiftFunctor C 1).obj obj) (d_squared : CategoryTheory.CategoryStruct.comp d ((CategoryTheory.shiftFunctor C 1).map d) = 0 := by cat_disch) : CategoryTheory.DifferentialObject S C
• CategoryTheory.DifferentialObject.mkIso_hom_f 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (f : X.obj ≅ Y.obj) (hf : CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f.hom) = CategoryTheory.CategoryStruct.comp f.hom Y.d) : (CategoryTheory.DifferentialObject.mkIso f hf).hom.f = f.hom
• CategoryTheory.DifferentialObject.mkIso_inv_f 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (f : X.obj ≅ Y.obj) (hf : CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f.hom) = CategoryTheory.CategoryStruct.comp f.hom Y.d) : (CategoryTheory.DifferentialObject.mkIso f hf).inv.f = f.inv
• CategoryTheory.DifferentialObject.d_squared 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (self : CategoryTheory.DifferentialObject S C) : CategoryTheory.CategoryStruct.comp self.d ((CategoryTheory.shiftFunctor C 1).map self.d) = 0
• CategoryTheory.Functor.mapDifferentialObject_obj_d 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (D : Type u') [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms D] [CategoryTheory.HasShift D S] (F : CategoryTheory.Functor C D) (η : (CategoryTheory.shiftFunctor C 1).comp F ⟶ F.comp (CategoryTheory.shiftFunctor D 1)) (hF : ∀ (c c' : C), F.map 0 = 0) (X : CategoryTheory.DifferentialObject S C) : ((CategoryTheory.Functor.mapDifferentialObject D F η hF).obj X).d = CategoryTheory.CategoryStruct.comp (F.map X.d) (η.app X.obj)
• CategoryTheory.DifferentialObject.d_squared_assoc 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (self : CategoryTheory.DifferentialObject S C) {Z : C} (h : (CategoryTheory.shiftFunctor C 1).obj ((CategoryTheory.shiftFunctor C 1).obj self.obj) ⟶ Z) : CategoryTheory.CategoryStruct.comp self.d (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C 1).map self.d) h) = CategoryTheory.CategoryStruct.comp 0 h
• CategoryTheory.DifferentialObject.shiftFunctor_obj_d 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (n : S) (X : CategoryTheory.DifferentialObject S C) : ((CategoryTheory.DifferentialObject.shiftFunctor C n).obj X).d = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).map X.d) (CategoryTheory.shiftComm X.obj 1 n).hom
• CategoryTheory.DifferentialObject.shiftZero_hom_app_f 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (X : CategoryTheory.DifferentialObject S C) : ((CategoryTheory.DifferentialObject.shiftZero C).hom.app X).f = (CategoryTheory.shiftFunctorZero C S).hom.app X.obj
• CategoryTheory.DifferentialObject.shiftZero_inv_app_f 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (X : CategoryTheory.DifferentialObject S C) : ((CategoryTheory.DifferentialObject.shiftZero C).inv.app X).f = (CategoryTheory.shiftFunctorZero C S).inv.app X.obj
• CategoryTheory.Functor.mapDifferentialObject_map_f 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (D : Type u') [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms D] [CategoryTheory.HasShift D S] (F : CategoryTheory.Functor C D) (η : (CategoryTheory.shiftFunctor C 1).comp F ⟶ F.comp (CategoryTheory.shiftFunctor D 1)) (hF : ∀ (c c' : C), F.map 0 = 0) {X✝ Y✝ : CategoryTheory.DifferentialObject S C} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Functor.mapDifferentialObject D F η hF).map f).f = F.map f.f
• CategoryTheory.DifferentialObject.shiftFunctorAdd_hom_app_f 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (m n : S) (X : CategoryTheory.DifferentialObject S C) : ((CategoryTheory.DifferentialObject.shiftFunctorAdd C m n).hom.app X).f = (CategoryTheory.shiftFunctorAdd C m n).hom.app X.obj
• CategoryTheory.DifferentialObject.shiftFunctorAdd_inv_app_f 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (m n : S) (X : CategoryTheory.DifferentialObject S C) : ((CategoryTheory.DifferentialObject.shiftFunctorAdd C m n).inv.app X).f = (CategoryTheory.shiftFunctorAdd C m n).inv.app X.obj
• CategoryTheory.DifferentialObject.shiftFunctor_map_f 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (n : S) {X✝ Y✝ : CategoryTheory.DifferentialObject S C} (f : X✝ ⟶ Y✝) : ((CategoryTheory.DifferentialObject.shiftFunctor C n).map f).f = (CategoryTheory.shiftFunctor C n).map f.f
• CategoryTheory.DifferentialObject.objEqToHom 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] {b : β} {V : Type u_2} [CategoryTheory.Category.{v_1, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) {i j : β} (h : i = j) : X.obj i ⟶ X.obj j
• HomologicalComplex.dgoEquivHomologicalComplex 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{v_1, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V) ≌ HomologicalComplex V (ComplexShape.up' b)
• HomologicalComplex.dgoToHomologicalComplex 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{v_1, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] : CategoryTheory.Functor (CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) (HomologicalComplex V (ComplexShape.up' b))
• HomologicalComplex.homologicalComplexToDGO 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{v_1, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] : CategoryTheory.Functor (HomologicalComplex V (ComplexShape.up' b)) (CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V))
• CategoryTheory.DifferentialObject.objEqToHom_refl 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] {b : β} {V : Type u_2} [CategoryTheory.Category.{v_1, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) (i : β) : X.objEqToHom ⋯ = CategoryTheory.CategoryStruct.id (X.obj i)
• HomologicalComplex.homologicalComplexToDGO_obj_obj 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{v_1, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex V (ComplexShape.up' b)) (i : β) : ((HomologicalComplex.homologicalComplexToDGO b V).obj X).obj i = X.X i
• HomologicalComplex.dgoToHomologicalComplex_obj_X 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{v_1, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) (i : β) : ((HomologicalComplex.dgoToHomologicalComplex b V).obj X).X i = X.obj i
• HomologicalComplex.dgoEquivHomologicalComplex_functor 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{v_1, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] : (HomologicalComplex.dgoEquivHomologicalComplex b V).functor = HomologicalComplex.dgoToHomologicalComplex b V
• HomologicalComplex.dgoEquivHomologicalComplex_inverse 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{v_1, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] : (HomologicalComplex.dgoEquivHomologicalComplex b V).inverse = HomologicalComplex.homologicalComplexToDGO b V
• HomologicalComplex.homologicalComplexToDGO_obj_d 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{v_1, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex V (ComplexShape.up' b)) (i : β) : ((HomologicalComplex.homologicalComplexToDGO b V).obj X).d i = X.d i ((fun b_1 => b_1 + { as := 1 }.as • b) i)
• HomologicalComplex.dgoEquivHomologicalComplexUnitIso 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{v_1, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] : CategoryTheory.Functor.id (CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) ≅ (HomologicalComplex.dgoToHomologicalComplex b V).comp (HomologicalComplex.homologicalComplexToDGO b V)
• HomologicalComplex.dgoEquivHomologicalComplexCounitIso 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{v_1, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] : (HomologicalComplex.homologicalComplexToDGO b V).comp (HomologicalComplex.dgoToHomologicalComplex b V) ≅ CategoryTheory.Functor.id (HomologicalComplex V (ComplexShape.up' b))
• CategoryTheory.DifferentialObject.eqToHom_f' 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] {b : β} {V : Type u_2} [CategoryTheory.Category.{v_1, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] {X Y : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)} (f : X ⟶ Y) {x y : β} (h : x = y) : CategoryTheory.CategoryStruct.comp (X.objEqToHom h) (f.f y) = CategoryTheory.CategoryStruct.comp (f.f x) (Y.objEqToHom h)
• HomologicalComplex.dgoEquivHomologicalComplex_unitIso 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{v_1, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] : (HomologicalComplex.dgoEquivHomologicalComplex b V).unitIso = HomologicalComplex.dgoEquivHomologicalComplexUnitIso b V
• HomologicalComplex.dgoEquivHomologicalComplex_counitIso 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{v_1, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] : (HomologicalComplex.dgoEquivHomologicalComplex b V).counitIso = HomologicalComplex.dgoEquivHomologicalComplexCounitIso b V
• CategoryTheory.DifferentialObject.eqToHom_f'_assoc 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] {b : β} {V : Type u_2} [CategoryTheory.Category.{v_1, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] {X Y : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)} (f : X ⟶ Y) {x y : β} (h : x = y) {Z : V} (h✝ : Y.obj y ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.objEqToHom h) (CategoryTheory.CategoryStruct.comp (f.f y) h✝) = CategoryTheory.CategoryStruct.comp (f.f x) (CategoryTheory.CategoryStruct.comp (Y.objEqToHom h) h✝)
• HomologicalComplex.homologicalComplexToDGO_map_f 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{v_1, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] {X Y : HomologicalComplex V (ComplexShape.up' b)} (f : X ⟶ Y) (i : β) : ((HomologicalComplex.homologicalComplexToDGO b V).map f).f i = f.f i
• CategoryTheory.DifferentialObject.objEqToHom_d 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] {b : β} {V : Type u_2} [CategoryTheory.Category.{v_1, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) {x y : β} (h : x = y) : CategoryTheory.CategoryStruct.comp (X.objEqToHom h) (X.d y) = CategoryTheory.CategoryStruct.comp (X.d x) (X.objEqToHom ⋯)
• CategoryTheory.DifferentialObject.objEqToHom_d_assoc 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] {b : β} {V : Type u_2} [CategoryTheory.Category.{v_1, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) {x y : β} (h : x = y) {Z : V} (h✝ : (CategoryTheory.shiftFunctor (CategoryTheory.GradedObjectWithShift b V) 1).obj X.obj y ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.objEqToHom h) (CategoryTheory.CategoryStruct.comp (X.d y) h✝) = CategoryTheory.CategoryStruct.comp (X.d x) (CategoryTheory.CategoryStruct.comp (X.objEqToHom ⋯) h✝)
• HomologicalComplex.dgoToHomologicalComplex_obj_d 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{v_1, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) (i j : β) : ((HomologicalComplex.dgoToHomologicalComplex b V).obj X).d i j = if h : i + b = j then CategoryTheory.CategoryStruct.comp (X.d i) (X.objEqToHom ⋯) else 0
• CategoryTheory.DifferentialObject.d_squared_apply 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] {b : β} {V : Type u_2} [CategoryTheory.Category.{v_1, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) {x : β} : CategoryTheory.CategoryStruct.comp (X.d x) (X.d ((fun b_1 => b_1 + { as := 1 }.as • b) x)) = 0
• HomologicalComplex.dgoEquivHomologicalComplexCounitIso_hom_app_f 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{v_1, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex V (ComplexShape.up' b)) (i : β) : ((HomologicalComplex.dgoEquivHomologicalComplexCounitIso b V).hom.app X).f i = CategoryTheory.CategoryStruct.id (X.X i)
• HomologicalComplex.dgoEquivHomologicalComplexCounitIso_inv_app_f 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{v_1, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex V (ComplexShape.up' b)) (i : β) : ((HomologicalComplex.dgoEquivHomologicalComplexCounitIso b V).inv.app X).f i = CategoryTheory.CategoryStruct.id (X.X i)
• CategoryTheory.DifferentialObject.d_squared_apply_assoc 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] {b : β} {V : Type u_2} [CategoryTheory.Category.{v_1, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) {x : β} {Z : V} (h : (CategoryTheory.shiftFunctor (CategoryTheory.GradedObjectWithShift b V) 1).obj X.obj (x + 1 • b) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.d x) (CategoryTheory.CategoryStruct.comp (X.d (x + 1 • b)) h) = CategoryTheory.CategoryStruct.comp 0 h
• HomologicalComplex.dgoEquivHomologicalComplexUnitIso_hom_app_f 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{v_1, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) (i : β) : ((HomologicalComplex.dgoEquivHomologicalComplexUnitIso b V).hom.app X).f i = CategoryTheory.CategoryStruct.id (X.obj i)
• HomologicalComplex.dgoEquivHomologicalComplexUnitIso_inv_app_f 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{v_1, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) (i : β) : ((HomologicalComplex.dgoEquivHomologicalComplexUnitIso b V).inv.app X).f i = CategoryTheory.CategoryStruct.id (X.obj i)
• HomologicalComplex.dgoToHomologicalComplex_map_f 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{v_1, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] {X Y : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)} (f : X ⟶ Y) (i : β) : ((HomologicalComplex.dgoToHomologicalComplex b V).map f).f i = f.f i

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 69fae59