Loogle!

Result

Found 1968 declarations mentioning CategoryTheory.Limits.HasZeroObject. Of these, only the first 200 are shown.

• CategoryTheory.Limits.HasZeroObject 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  (C : Type u) [CategoryTheory.Category.{v, u} C] : Prop
• CategoryTheory.Limits.hasZeroObject_pUnit 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  : CategoryTheory.Limits.HasZeroObject (CategoryTheory.Discrete PUnit.{u_1 + 1})
• CategoryTheory.Limits.HasZeroObject.zero' 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] : Zero C
• CategoryTheory.Limits.HasZeroObject.hasInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.Limits.HasInitial C
• CategoryTheory.Limits.HasZeroObject.hasTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.Limits.HasTerminal C
• CategoryTheory.Limits.HasZeroObject.initialMonoClass 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.Limits.InitialMonoClass C
• CategoryTheory.Limits.IsZero.hasZeroObject 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (hX : CategoryTheory.Limits.IsZero X) : CategoryTheory.Limits.HasZeroObject C
• CategoryTheory.Limits.hasZeroObject_op 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.Limits.HasZeroObject Cᵒᵖ
• CategoryTheory.Limits.hasZeroObject_unop 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject Cᵒᵖ] : CategoryTheory.Limits.HasZeroObject C
• CategoryTheory.Limits.HasZeroObject.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] (zero : ∃ X, CategoryTheory.Limits.IsZero X) : CategoryTheory.Limits.HasZeroObject C
• CategoryTheory.Limits.HasZeroObject.zero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Limits.HasZeroObject C] : ∃ X, CategoryTheory.Limits.IsZero X
• CategoryTheory.Limits.isZero_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.Limits.IsZero 0
• CategoryTheory.Limits.HasZeroObject.zeroIsInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.Limits.IsInitial 0
• CategoryTheory.Limits.HasZeroObject.zeroIsTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.Limits.IsTerminal 0
• CategoryTheory.Limits.HasZeroObject.instSubsingletonIsoOfNat 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] (X : C) : Subsingleton (X ≅ 0)
• CategoryTheory.Limits.HasZeroObject.zeroIsoIsInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] {X : C} (t : CategoryTheory.Limits.IsInitial X) : 0 ≅ X
• CategoryTheory.Limits.HasZeroObject.zeroIsoIsTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] {X : C} (t : CategoryTheory.Limits.IsTerminal X) : 0 ≅ X
• CategoryTheory.Limits.IsZero.isoZero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] {X : C} (hX : CategoryTheory.Limits.IsZero X) : X ≅ 0
• CategoryTheory.Limits.HasZeroObject.uniqueFrom 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] (X : C) : Unique (X ⟶ 0)
• CategoryTheory.Limits.HasZeroObject.uniqueTo 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] (X : C) : Unique (0 ⟶ X)
• CategoryTheory.Limits.HasZeroObject.zeroIsoInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasInitial C] : 0 ≅ ⊥_ C
• CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasTerminal C] : 0 ≅ ⊤_ C
• CategoryTheory.instEpiFromTerminalIsTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (A : C) [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.Epi (CategoryTheory.Limits.terminalIsTerminal.from A)
• CategoryTheory.Limits.IsZero.obj 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroObject D] {F : CategoryTheory.Functor C D} (hF : CategoryTheory.Limits.IsZero F) (X : C) : CategoryTheory.Limits.IsZero (F.obj X)
• CategoryTheory.Functor.isZero_iff 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroObject D] (F : CategoryTheory.Functor C D) : CategoryTheory.Limits.IsZero F ↔ ∀ (X : C), CategoryTheory.Limits.IsZero (F.obj X)
• CategoryTheory.Limits.HasZeroObject.instEpi 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] {X : C} (f : X ⟶ 0) : CategoryTheory.Epi f
• CategoryTheory.Limits.HasZeroObject.instMono 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] {X : C} (f : 0 ⟶ X) : CategoryTheory.Mono f
• CategoryTheory.Limits.HasZeroObject.zero_to_zero_isIso 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] (f : 0 ⟶ 0) : CategoryTheory.IsIso f
• CategoryTheory.Limits.HasZeroObject.from_zero_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] {X : C} (f g : 0 ⟶ X) : f = g
• CategoryTheory.Limits.HasZeroObject.to_zero_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] {X : C} (f g : X ⟶ 0) : f = g
• CategoryTheory.Limits.HasZeroObject.from_zero_ext_iff 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {f g : 0 ⟶ X} : f = g ↔ True
• CategoryTheory.Limits.HasZeroObject.to_zero_ext_iff 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {f g : X ⟶ 0} : f = g ↔ True
• CategoryTheory.Limits.HasZeroObject.zeroMorphismsOfZeroObject 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.Limits.HasZeroMorphisms C
• CategoryTheory.Limits.hasZeroObject_of_hasInitial_object 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasInitial C] : CategoryTheory.Limits.HasZeroObject C
• CategoryTheory.Limits.hasZeroObject_of_hasTerminal_object 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.Limits.HasZeroObject C
• CategoryTheory.Limits.HasZeroObject.instFunctor 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] {B : Type u_1} [CategoryTheory.Category.{v_1, u_1} B] : CategoryTheory.Limits.HasZeroObject (CategoryTheory.Functor B C)
• CategoryTheory.Limits.isoOfIsIsomorphicZero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X : C} (P : CategoryTheory.IsIsomorphic X 0) : X ≅ 0
• CategoryTheory.Limits.epi_of_target_iso_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) (i : Y ≅ 0) : CategoryTheory.Epi f
• CategoryTheory.Limits.mono_of_source_iso_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) (i : X ≅ 0) : CategoryTheory.Mono f
• CategoryTheory.Limits.hasImage_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {X Y : C} : CategoryTheory.Limits.HasImage 0
• CategoryTheory.Limits.imageFactorisationZero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (X Y : C) : CategoryTheory.Limits.ImageFactorisation 0
• CategoryTheory.Limits.monoFactorisationZero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (X Y : C) : CategoryTheory.Limits.MonoFactorisation 0
• CategoryTheory.Functor.zero_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroObject D] (X : C) : CategoryTheory.Limits.IsZero (CategoryTheory.Functor.obj 0 X)
• CategoryTheory.Limits.isIso_of_source_target_iso_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {X Y : C} (f : X ⟶ Y) (i : X ≅ 0) (j : Y ≅ 0) : CategoryTheory.IsIso f
• CategoryTheory.Limits.IsColimit.isZero_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {F : CategoryTheory.Functor D C} {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) (hF : CategoryTheory.Limits.IsZero F) : CategoryTheory.Limits.IsZero c.pt
• CategoryTheory.Limits.IsColimit.ofIsZero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {F : CategoryTheory.Functor D C} (c : CategoryTheory.Limits.Cocone F) (hF : CategoryTheory.Limits.IsZero F) (hc : CategoryTheory.Limits.IsZero c.pt) : CategoryTheory.Limits.IsColimit c
• CategoryTheory.Limits.IsLimit.isZero_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {F : CategoryTheory.Functor D C} {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) (hF : CategoryTheory.Limits.IsZero F) : CategoryTheory.Limits.IsZero c.pt
• CategoryTheory.Limits.IsLimit.ofIsZero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {F : CategoryTheory.Functor D C} (c : CategoryTheory.Limits.Cone F) (hF : CategoryTheory.Limits.IsZero F) (hc : CategoryTheory.Limits.IsZero c.pt) : CategoryTheory.Limits.IsLimit c
• CategoryTheory.Limits.isIsoZero_iff_source_target_isZero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (X Y : C) : CategoryTheory.IsIso 0 ↔ CategoryTheory.Limits.IsZero X ∧ CategoryTheory.Limits.IsZero Y
• CategoryTheory.Limits.isIsoZeroSelfEquivIsoZero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (X : C) : CategoryTheory.IsIso 0 ≃ (X ≅ 0)
• CategoryTheory.Limits.isoZeroOfEpiZero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} : CategoryTheory.Epi 0 → (Y ≅ 0)
• CategoryTheory.Limits.isoZeroOfMonoZero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} : CategoryTheory.Mono 0 → (X ≅ 0)
• CategoryTheory.Limits.monoFactorisationZero_I 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (X Y : C) : (CategoryTheory.Limits.monoFactorisationZero X Y).I = 0
• CategoryTheory.Limits.imageZero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {X Y : C} : CategoryTheory.Limits.image 0 ≅ 0
• CategoryTheory.Limits.idZeroEquivIsoZero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) : CategoryTheory.CategoryStruct.id X = 0 ≃ (X ≅ 0)
• CategoryTheory.Limits.isIsoZeroEquivIsoZero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (X Y : C) : CategoryTheory.IsIso 0 ≃ (X ≅ 0) × (Y ≅ 0)
• CategoryTheory.Limits.zero_of_source_iso_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) (i : X ≅ 0) : f = 0
• CategoryTheory.Limits.zero_of_source_iso_zero' 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) (i : CategoryTheory.IsIsomorphic X 0) : f = 0
• CategoryTheory.Limits.zero_of_target_iso_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) (i : Y ≅ 0) : f = 0
• CategoryTheory.Limits.zero_of_target_iso_zero' 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) (i : CategoryTheory.IsIsomorphic Y 0) : f = 0
• CategoryTheory.Limits.isoZeroOfEpiEqZero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.Epi f] (h : f = 0) : Y ≅ 0
• CategoryTheory.Limits.isoZeroOfMonoEqZero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.Mono f] (h : f = 0) : X ≅ 0
• CategoryTheory.Limits.imageZero' 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {X Y : C} {f : X ⟶ Y} (h : f = 0) [CategoryTheory.Limits.HasImage f] : CategoryTheory.Limits.image f ≅ 0
• CategoryTheory.Limits.zero_of_from_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X : C} (f : 0 ⟶ X) : f = 0
• CategoryTheory.Limits.zero_of_to_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X : C} (f : X ⟶ 0) : f = 0
• CategoryTheory.Limits.HasZeroObject.zeroIsoIsInitial_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X : C} (t : CategoryTheory.Limits.IsInitial X) : (CategoryTheory.Limits.HasZeroObject.zeroIsoIsInitial t).hom = 0
• CategoryTheory.Limits.HasZeroObject.zeroIsoIsInitial_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X : C} (t : CategoryTheory.Limits.IsInitial X) : (CategoryTheory.Limits.HasZeroObject.zeroIsoIsInitial t).inv = 0
• CategoryTheory.Limits.HasZeroObject.zeroIsoIsTerminal_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X : C} (t : CategoryTheory.Limits.IsTerminal X) : (CategoryTheory.Limits.HasZeroObject.zeroIsoIsTerminal t).hom = 0
• CategoryTheory.Limits.HasZeroObject.zeroIsoIsTerminal_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X : C} (t : CategoryTheory.Limits.IsTerminal X) : (CategoryTheory.Limits.HasZeroObject.zeroIsoIsTerminal t).inv = 0
• CategoryTheory.Limits.HasZeroObject.zeroIsoInitial_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasInitial C] : CategoryTheory.Limits.HasZeroObject.zeroIsoInitial.hom = 0
• CategoryTheory.Limits.HasZeroObject.zeroIsoInitial_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasInitial C] : CategoryTheory.Limits.HasZeroObject.zeroIsoInitial.inv = 0
• CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal.hom = 0
• CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal.inv = 0
• CategoryTheory.Limits.monoFactorisationZero_e 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (X Y : C) : (CategoryTheory.Limits.monoFactorisationZero X Y).e = 0
• CategoryTheory.Limits.monoFactorisationZero_m 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (X Y : C) : (CategoryTheory.Limits.monoFactorisationZero X Y).m = 0
• CategoryTheory.Limits.id_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] : CategoryTheory.CategoryStruct.id 0 = 0
• CategoryTheory.Limits.isoZeroOfEpiZero_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (x✝ : CategoryTheory.Epi 0) : (CategoryTheory.Limits.isoZeroOfEpiZero x✝).hom = 0
• CategoryTheory.Limits.isoZeroOfEpiZero_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (x✝ : CategoryTheory.Epi 0) : (CategoryTheory.Limits.isoZeroOfEpiZero x✝).inv = 0
• CategoryTheory.Limits.isoZeroOfMonoZero_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (x✝ : CategoryTheory.Mono 0) : (CategoryTheory.Limits.isoZeroOfMonoZero x✝).hom = 0
• CategoryTheory.Limits.isoZeroOfMonoZero_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (x✝ : CategoryTheory.Mono 0) : (CategoryTheory.Limits.isoZeroOfMonoZero x✝).inv = 0
• CategoryTheory.Limits.IsZero.map 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms D] {F : CategoryTheory.Functor C D} (hF : CategoryTheory.Limits.IsZero F) {X Y : C} (f : X ⟶ Y) : F.map f = 0
• CategoryTheory.Limits.image.ι_zero' 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasEqualizers C] {X Y : C} {f : X ⟶ Y} (h : f = 0) [CategoryTheory.Limits.HasImage f] : CategoryTheory.Limits.image.ι f = 0
• CategoryTheory.Limits.image.ι_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {X Y : C} [CategoryTheory.Limits.HasImage 0] : CategoryTheory.Limits.image.ι 0 = 0
• CategoryTheory.zero_map 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms D] {X Y : C} (f : X ⟶ Y) : CategoryTheory.Functor.map 0 f = 0
• CategoryTheory.Limits.idZeroEquivIsoZero_apply_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) (h : CategoryTheory.CategoryStruct.id X = 0) : ((CategoryTheory.Limits.idZeroEquivIsoZero X) h).hom = 0
• CategoryTheory.Limits.idZeroEquivIsoZero_apply_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) (h : CategoryTheory.CategoryStruct.id X = 0) : ((CategoryTheory.Limits.idZeroEquivIsoZero X) h).inv = 0
• SemimoduleCat.instHasZeroObject 📋 Mathlib.Algebra.Category.ModuleCat.Semi
  {R : Type u} [Semiring R] : CategoryTheory.Limits.HasZeroObject (SemimoduleCat R)
• CategoryTheory.Functor.preservesColimitsOfSize_of_isZero 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D) (hG : CategoryTheory.Limits.IsZero G) : CategoryTheory.Limits.PreservesColimitsOfSize.{v, u, v₁, v₂, u₁, u₂} G
• CategoryTheory.Functor.preservesLimitsOfSize_of_isZero 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D) (hG : CategoryTheory.Limits.IsZero G) : CategoryTheory.Limits.PreservesLimitsOfSize.{v, u, v₁, v₂, u₁, u₂} G
• CategoryTheory.Functor.preservesColimitsOfShape_of_isZero 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D) (hG : CategoryTheory.Limits.IsZero G) (J : Type u_1) [CategoryTheory.Category.{v_1, u_1} J] : CategoryTheory.Limits.PreservesColimitsOfShape J G
• CategoryTheory.Functor.preservesLimitsOfShape_of_isZero 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D) (hG : CategoryTheory.Limits.IsZero G) (J : Type u_1) [CategoryTheory.Category.{v_1, u_1} J] : CategoryTheory.Limits.PreservesLimitsOfShape J G
• CategoryTheory.Functor.preservesInitialObject_of_preservesZeroMorphisms 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) F
• CategoryTheory.Functor.preservesTerminalObject_of_preservesZeroMorphisms 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) F
• CategoryTheory.Functor.preservesZeroMorphisms_of_preserves_initial_object 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {F : CategoryTheory.Functor C D} [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) F] : F.PreservesZeroMorphisms
• CategoryTheory.Functor.preservesZeroMorphisms_of_preserves_terminal_object 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {F : CategoryTheory.Functor C D} [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) F] : F.PreservesZeroMorphisms
• CategoryTheory.Functor.mapZeroObject 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] : F.obj 0 ≅ 0
• CategoryTheory.Functor.preservesZeroMorphisms_of_map_zero_object 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {F : CategoryTheory.Functor C D} (i : F.obj 0 ≅ 0) : F.PreservesZeroMorphisms
• CategoryTheory.Functor.mapZeroObject_hom 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] : F.mapZeroObject.hom = 0
• CategoryTheory.Functor.mapZeroObject_inv 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] : F.mapZeroObject.inv = 0
• CategoryTheory.Limits.cokernel.zeroCokernelCofork 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.Limits.CokernelCofork f
• CategoryTheory.Limits.kernel.zeroKernelFork 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.Limits.KernelFork f
• CategoryTheory.Limits.cokernel.ofEpi 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasCokernel f] [CategoryTheory.Epi f] : CategoryTheory.Limits.cokernel f ≅ 0
• CategoryTheory.Limits.kernel.ofMono 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasKernel f] [CategoryTheory.Mono f] : CategoryTheory.Limits.kernel f ≅ 0
• CategoryTheory.Limits.cokernel.isColimitCoconeZeroCocone 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Epi f] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.cokernel.zeroCokernelCofork f)
• CategoryTheory.Limits.kernel.isLimitConeZeroCone 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Mono f] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.kernel.zeroKernelFork f)
• CategoryTheory.Limits.cokernel.zeroCokernelCofork_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasZeroObject C] : (CategoryTheory.Limits.cokernel.zeroCokernelCofork f).pt = 0
• CategoryTheory.Limits.kernel.zeroKernelFork_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasZeroObject C] : (CategoryTheory.Limits.kernel.zeroKernelFork f).pt = 0
• CategoryTheory.Limits.cokernel.of_kernel_of_mono 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasKernel f] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)] [CategoryTheory.Mono f] : CategoryTheory.IsIso (CategoryTheory.Limits.cokernel.π (CategoryTheory.Limits.kernel.ι f))
• CategoryTheory.Limits.kernel.of_cokernel_of_epi 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasCokernel f] [CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)] [CategoryTheory.Epi f] : CategoryTheory.IsIso (CategoryTheory.Limits.kernel.ι (CategoryTheory.Limits.cokernel.π f))
• CategoryTheory.Limits.cokernel.π_of_epi 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasCokernel f] [CategoryTheory.Epi f] : CategoryTheory.Limits.cokernel.π f = 0
• CategoryTheory.Limits.kernel.ι_of_mono 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasKernel f] [CategoryTheory.Mono f] : CategoryTheory.Limits.kernel.ι f = 0
• CategoryTheory.Limits.cokernel.zeroCokernelCofork_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.Limits.Cofork.π (CategoryTheory.Limits.cokernel.zeroCokernelCofork f) = 0
• CategoryTheory.Limits.kernel.zeroKernelFork_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.Limits.Fork.ι (CategoryTheory.Limits.kernel.zeroKernelFork f) = 0
• CategoryTheory.Limits.zeroCokernelOfZeroCancel 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {X Y : C} (f : X ⟶ Y) (hf : ∀ (Z : C) (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp f g = 0 → g = 0) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ 0 ⋯)
• CategoryTheory.Limits.zeroKernelOfCancelZero 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {X Y : C} (f : X ⟶ Y) (hf : ∀ (Z : C) (g : Z ⟶ X), CategoryTheory.CategoryStruct.comp g f = 0 → g = 0) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι 0 ⋯)
• CategoryTheory.Preadditive.hasZeroObject_of_hasCoproduct 📋 Mathlib.CategoryTheory.Preadditive.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproduct PEmpty.elim] : CategoryTheory.Limits.HasZeroObject C
• CategoryTheory.Preadditive.epi_of_cokernel_iso_zero 📋 Mathlib.CategoryTheory.Preadditive.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.parallelPair f 0)] (w : CategoryTheory.Limits.cokernel f ≅ 0) : CategoryTheory.Epi f
• CategoryTheory.Preadditive.mono_of_kernel_iso_zero 📋 Mathlib.CategoryTheory.Preadditive.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair f 0)] (w : CategoryTheory.Limits.kernel f ≅ 0) : CategoryTheory.Mono f
• CategoryTheory.Limits.hasZeroObject_of_hasFiniteBiproducts 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] : CategoryTheory.Limits.HasZeroObject C
• CategoryTheory.Functor.hasZeroObject_of_additive 📋 Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.Limits.HasZeroObject D
• CategoryTheory.Functor.instAdditiveOfNat 📋 Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] : CategoryTheory.Functor.Additive 0
• CategoryTheory.AdditiveFunctor.ofExact 📋 Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
  (C : Type u₁) (D : Type u₂) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts C] : CategoryTheory.Functor (C ⥤ₑ D) (C ⥤+ D)
• CategoryTheory.AdditiveFunctor.ofLeftExact 📋 Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
  (C : Type u₁) (D : Type u₂) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts C] : CategoryTheory.Functor (C ⥤ₗ D) (C ⥤+ D)
• CategoryTheory.AdditiveFunctor.ofRightExact 📋 Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
  (C : Type u₁) (D : Type u₂) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts C] : CategoryTheory.Functor (C ⥤ᵣ D) (C ⥤+ D)
• CategoryTheory.exactFunctor_le_additiveFunctor 📋 Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
  (C : Type u₁) (D : Type u₂) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts C] : CategoryTheory.exactFunctor C D ≤ CategoryTheory.additiveFunctor C D
• CategoryTheory.leftExactFunctor_le_additiveFunctor 📋 Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
  (C : Type u₁) (D : Type u₂) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts C] : CategoryTheory.leftExactFunctor C D ≤ CategoryTheory.additiveFunctor C D
• CategoryTheory.rightExactFunctor_le_additiveFunctor 📋 Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
  (C : Type u₁) (D : Type u₂) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts C] : CategoryTheory.rightExactFunctor C D ≤ CategoryTheory.additiveFunctor C D
• CategoryTheory.AdditiveFunctor.ofExact_obj_fst 📋 Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts C] (F : C ⥤ₑ D) : ((CategoryTheory.AdditiveFunctor.ofExact C D).obj F).obj = F.obj
• CategoryTheory.AdditiveFunctor.ofLeftExact_obj_fst 📋 Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts C] (F : C ⥤ₗ D) : ((CategoryTheory.AdditiveFunctor.ofLeftExact C D).obj F).obj = F.obj
• CategoryTheory.AdditiveFunctor.ofRightExact_obj_fst 📋 Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts C] (F : C ⥤ᵣ D) : ((CategoryTheory.AdditiveFunctor.ofRightExact C D).obj F).obj = F.obj
• CategoryTheory.AdditiveFunctor.ofExact_map_hom 📋 Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts C] {F G : C ⥤ₑ D} (α : F ⟶ G) : ((CategoryTheory.AdditiveFunctor.ofExact C D).map α).hom = α.hom
• CategoryTheory.AdditiveFunctor.ofLeftExact_map_hom 📋 Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts C] {F G : C ⥤ₗ D} (α : F ⟶ G) : ((CategoryTheory.AdditiveFunctor.ofLeftExact C D).map α).hom = α.hom
• CategoryTheory.AdditiveFunctor.ofRightExact_map_hom 📋 Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts C] {F G : C ⥤ᵣ D} (α : F ⟶ G) : ((CategoryTheory.AdditiveFunctor.ofRightExact C D).map α).hom = α.hom
• ModuleCat.instHasZeroObject 📋 Mathlib.Algebra.Category.ModuleCat.Basic
  {R : Type u} [Ring R] : CategoryTheory.Limits.HasZeroObject (ModuleCat R)
• CategoryTheory.ObjectProperty.instContainsZeroIsZeroOfHasZeroObject 📋 Mathlib.CategoryTheory.ObjectProperty.ContainsZero
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.ObjectProperty.ContainsZero CategoryTheory.Limits.IsZero
• CategoryTheory.ObjectProperty.instHasZeroObjectFullSubcategoryOfContainsZero 📋 Mathlib.CategoryTheory.ObjectProperty.ContainsZero
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.ContainsZero] : CategoryTheory.Limits.HasZeroObject P.FullSubcategory
• CategoryTheory.ObjectProperty.instContainsZeroTopOfHasZeroObject 📋 Mathlib.CategoryTheory.ObjectProperty.ContainsZero
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] : ⊤.ContainsZero
• CategoryTheory.ObjectProperty.prop_zero 📋 Mathlib.CategoryTheory.ObjectProperty.ContainsZero
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.ContainsZero] [P.IsClosedUnderIsomorphisms] [CategoryTheory.Limits.HasZeroObject C] : P 0
• CategoryTheory.ObjectProperty.instContainsZeroInverseImageOfIsClosedUnderIsomorphismsOfPreservesZeroMorphismsOfHasZeroObject 📋 Mathlib.CategoryTheory.ObjectProperty.ContainsZero
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty C) [P.ContainsZero] [P.IsClosedUnderIsomorphisms] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor D C) [F.PreservesZeroMorphisms] [CategoryTheory.Limits.HasZeroObject D] : (P.inverseImage F).ContainsZero
• CategoryTheory.ObjectProperty.IsStableUnderRetracts.containsZero 📋 Mathlib.CategoryTheory.ObjectProperty.Retract
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.IsStableUnderRetracts] [CategoryTheory.Limits.HasZeroObject C] {X : C} (h : P X) : P.ContainsZero
• CategoryTheory.ObjectProperty.IsStableUnderRetracts.instContainsZeroOfHasZeroObjectOfNonempty 📋 Mathlib.CategoryTheory.ObjectProperty.Retract
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.IsStableUnderRetracts] [CategoryTheory.Limits.HasZeroObject C] [P.Nonempty] : P.ContainsZero
• CategoryTheory.AddMon.instHasZeroObject 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
  {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.SemiCartesianMonoidalCategory D] : CategoryTheory.Limits.HasZeroObject (CategoryTheory.AddMon D)
• CategoryTheory.Mon.instHasZeroObject 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
  {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.SemiCartesianMonoidalCategory D] : CategoryTheory.Limits.HasZeroObject (CategoryTheory.Mon D)
• CategoryTheory.AddGrp.instHasZeroObject 📋 Mathlib.CategoryTheory.Monoidal.Grp
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] : CategoryTheory.Limits.HasZeroObject (CategoryTheory.AddGrp C)
• CategoryTheory.Grp.instHasZeroObject 📋 Mathlib.CategoryTheory.Monoidal.Grp
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] : CategoryTheory.Limits.HasZeroObject (CategoryTheory.Grp C)
• CategoryTheory.Limits.mapZeroCokernelCofork 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D) [G.PreservesZeroMorphisms] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.Limits.cokernel.zeroCokernelCofork f).map G ≅ CategoryTheory.Limits.cokernel.zeroCokernelCofork (G.map f)
• CategoryTheory.Limits.mapZeroKernelFork 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D) [G.PreservesZeroMorphisms] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.Limits.kernel.zeroKernelFork f).map G ≅ CategoryTheory.Limits.kernel.zeroKernelFork (G.map f)
• CategoryTheory.NormalEpiCategory.preservesMonomorphisms_of_preservesKernels 📋 Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.IsNormalEpiCategory C] [CategoryTheory.Limits.HasZeroObject C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms D] [CategoryTheory.Limits.HasZeroObject D] (F : CategoryTheory.Functor D C) [F.PreservesZeroMorphisms] [∀ {X Y : D} (f : X ⟶ Y), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F] : F.PreservesMonomorphisms
• CategoryTheory.NormalMonoCategory.preservesEpimorphisms_of_preservesCokernels 📋 Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.IsNormalMonoCategory C] [CategoryTheory.Limits.HasZeroObject C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms D] [CategoryTheory.Limits.HasZeroObject D] (F : CategoryTheory.Functor D C) [F.PreservesZeroMorphisms] [∀ {X Y : D} (f : X ⟶ Y), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F] : F.PreservesEpimorphisms
• CategoryTheory.NormalEpiCategory.mono_of_cancel_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.IsNormalEpiCategory C] [CategoryTheory.Limits.HasZeroObject C] {X Y : C} (f : X ⟶ Y) (hf : ∀ (Z : C) (g : Z ⟶ X), CategoryTheory.CategoryStruct.comp g f = 0 → g = 0) : CategoryTheory.Mono f
• CategoryTheory.NormalMonoCategory.epi_of_zero_cancel 📋 Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.IsNormalMonoCategory C] [CategoryTheory.Limits.HasZeroObject C] {X Y : C} (f : X ⟶ Y) (hf : ∀ (Z : C) (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp f g = 0 → g = 0) : CategoryTheory.Epi f
• CategoryTheory.NonPreadditiveAbelian.has_zero_object 📋 Mathlib.CategoryTheory.Abelian.NonPreadditive
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.NonPreadditiveAbelian C] : CategoryTheory.Limits.HasZeroObject C
• CategoryTheory.NonPreadditiveAbelian.mk 📋 Mathlib.CategoryTheory.Abelian.NonPreadditive
  {C : Type u} [CategoryTheory.Category.{v, u} C] [toHasZeroMorphisms : CategoryTheory.Limits.HasZeroMorphisms C] [toIsNormalMonoCategory : CategoryTheory.IsNormalMonoCategory C] [toIsNormalEpiCategory : CategoryTheory.IsNormalEpiCategory C] [has_zero_object : CategoryTheory.Limits.HasZeroObject C] [has_kernels : CategoryTheory.Limits.HasKernels C] [has_cokernels : CategoryTheory.Limits.HasCokernels C] [has_finite_products : CategoryTheory.Limits.HasFiniteProducts C] [has_finite_coproducts : CategoryTheory.Limits.HasFiniteCoproducts C] : CategoryTheory.NonPreadditiveAbelian C
• CategoryTheory.Abelian.hasZeroObject 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : CategoryTheory.Limits.HasZeroObject C
• CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.instIsIsoMImageMonoFactorisationOfHasZeroObjectOfEpi 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.Limits.HasZeroObject C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f] : CategoryTheory.IsIso (CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation f).m
• CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.instIsIsoEImageMonoFactorisationOfHasZeroObjectOfMonoOfCoimageImageComparison 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.Limits.HasZeroObject C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] [CategoryTheory.IsIso (CategoryTheory.Abelian.coimageImageComparison f)] : CategoryTheory.IsIso (CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation f).e
• CategoryTheory.Projective.zero_projective 📋 Mathlib.CategoryTheory.Preadditive.Projective.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.Projective 0
• CategoryTheory.Injective.zero_injective 📋 Mathlib.CategoryTheory.Preadditive.Injective.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.Injective 0
• CategoryTheory.ShortComplex.Exact.hasZeroObject 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : S.Exact) : CategoryTheory.Limits.HasZeroObject C
• CategoryTheory.ShortComplex.Splitting.exact 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} [CategoryTheory.Limits.HasZeroObject C] (s : S.Splitting) : S.Exact
• CategoryTheory.ShortComplex.Splitting.homologyData 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} [CategoryTheory.Limits.HasZeroObject C] (s : S.Splitting) : S.HomologyData
• CategoryTheory.ShortComplex.Splitting.leftHomologyData 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} [CategoryTheory.Limits.HasZeroObject C] (s : S.Splitting) : S.LeftHomologyData
• CategoryTheory.ShortComplex.Splitting.rightHomologyData 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} [CategoryTheory.Limits.HasZeroObject C] (s : S.Splitting) : S.RightHomologyData
• CategoryTheory.ShortComplex.exact_iff_homology_iso_zero 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [S.HasHomology] [CategoryTheory.Limits.HasZeroObject C] : S.Exact ↔ Nonempty (S.homology ≅ 0)
• CategoryTheory.ShortComplex.Splitting.leftHomologyData_K 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} [CategoryTheory.Limits.HasZeroObject C] (s : S.Splitting) : s.leftHomologyData.K = S.X₁
• CategoryTheory.ShortComplex.Splitting.rightHomologyData_Q 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} [CategoryTheory.Limits.HasZeroObject C] (s : S.Splitting) : s.rightHomologyData.Q = S.X₃
• CategoryTheory.ShortComplex.Splitting.leftHomologyData_H 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} [CategoryTheory.Limits.HasZeroObject C] (s : S.Splitting) : s.leftHomologyData.H = 0
• CategoryTheory.ShortComplex.Splitting.rightHomologyData_H 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} [CategoryTheory.Limits.HasZeroObject C] (s : S.Splitting) : s.rightHomologyData.H = 0
• CategoryTheory.ShortComplex.Splitting.homologyData_left 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} [CategoryTheory.Limits.HasZeroObject C] (s : S.Splitting) : s.homologyData.left = s.leftHomologyData
• CategoryTheory.ShortComplex.Splitting.homologyData_right 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} [CategoryTheory.Limits.HasZeroObject C] (s : S.Splitting) : s.homologyData.right = s.rightHomologyData
• CategoryTheory.Functor.instPreservesEpimorphisms 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [F.PreservesZeroMorphisms] [F.PreservesHomology] : F.PreservesEpimorphisms
• CategoryTheory.Functor.instPreservesMonomorphisms 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [F.PreservesZeroMorphisms] [F.PreservesHomology] : F.PreservesMonomorphisms
• CategoryTheory.ShortComplex.Splitting.leftHomologyData_i 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} [CategoryTheory.Limits.HasZeroObject C] (s : S.Splitting) : s.leftHomologyData.i = S.f
• CategoryTheory.ShortComplex.Splitting.rightHomologyData_p 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} [CategoryTheory.Limits.HasZeroObject C] (s : S.Splitting) : s.rightHomologyData.p = S.g
• CategoryTheory.ShortComplex.Splitting.homologyData_iso 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} [CategoryTheory.Limits.HasZeroObject C] (s : S.Splitting) : s.homologyData.iso = CategoryTheory.Iso.refl 0
• CategoryTheory.ShortComplex.Splitting.leftHomologyData_π 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} [CategoryTheory.Limits.HasZeroObject C] (s : S.Splitting) : s.leftHomologyData.π = 0
• CategoryTheory.ShortComplex.Splitting.rightHomologyData_ι 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} [CategoryTheory.Limits.HasZeroObject C] (s : S.Splitting) : s.rightHomologyData.ι = 0
• CategoryTheory.ShortComplex.exact_iff_epi 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.Limits.HasZeroObject C] (hg : S.g = 0) : S.Exact ↔ CategoryTheory.Epi S.f
• CategoryTheory.ShortComplex.exact_iff_mono 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.Limits.HasZeroObject C] (hf : S.f = 0) : S.Exact ↔ CategoryTheory.Mono S.g
• CategoryTheory.ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (hS : S.Exact) [CategoryTheory.Limits.HasZeroObject C] (kf : CategoryTheory.Limits.KernelFork S.g) (hkf : CategoryTheory.Limits.IsLimit kf) : S.LeftHomologyData
• CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (hS : S.Exact) [CategoryTheory.Limits.HasZeroObject C] (cc : CategoryTheory.Limits.CokernelCofork S.f) (hcc : CategoryTheory.Limits.IsColimit cc) : S.RightHomologyData
• CategoryTheory.ShortComplex.Splitting.fIsKernel 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} [CategoryTheory.Limits.HasZeroObject C] (s : S.Splitting) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι S.f ⋯)
• CategoryTheory.ShortComplex.Splitting.gIsCokernel 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} [CategoryTheory.Limits.HasZeroObject C] (s : S.Splitting) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ S.g ⋯)
• CategoryTheory.ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_H 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (hS : S.Exact) [CategoryTheory.Limits.HasZeroObject C] (kf : CategoryTheory.Limits.KernelFork S.g) (hkf : CategoryTheory.Limits.IsLimit kf) : (hS.leftHomologyDataOfIsLimitKernelFork kf hkf).H = 0
• CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_H 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (hS : S.Exact) [CategoryTheory.Limits.HasZeroObject C] (cc : CategoryTheory.Limits.CokernelCofork S.f) (hcc : CategoryTheory.Limits.IsColimit cc) : (hS.rightHomologyDataOfIsColimitCokernelCofork cc hcc).H = 0
• CategoryTheory.ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_K 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (hS : S.Exact) [CategoryTheory.Limits.HasZeroObject C] (kf : CategoryTheory.Limits.KernelFork S.g) (hkf : CategoryTheory.Limits.IsLimit kf) : (hS.leftHomologyDataOfIsLimitKernelFork kf hkf).K = kf.pt
• CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_Q 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (hS : S.Exact) [CategoryTheory.Limits.HasZeroObject C] (cc : CategoryTheory.Limits.CokernelCofork S.f) (hcc : CategoryTheory.Limits.IsColimit cc) : (hS.rightHomologyDataOfIsColimitCokernelCofork cc hcc).Q = cc.pt
• CategoryTheory.ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_i 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (hS : S.Exact) [CategoryTheory.Limits.HasZeroObject C] (kf : CategoryTheory.Limits.KernelFork S.g) (hkf : CategoryTheory.Limits.IsLimit kf) : (hS.leftHomologyDataOfIsLimitKernelFork kf hkf).i = CategoryTheory.Limits.Fork.ι kf
• CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_p 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (hS : S.Exact) [CategoryTheory.Limits.HasZeroObject C] (cc : CategoryTheory.Limits.CokernelCofork S.f) (hcc : CategoryTheory.Limits.IsColimit cc) : (hS.rightHomologyDataOfIsColimitCokernelCofork cc hcc).p = CategoryTheory.Limits.Cofork.π cc
• CategoryTheory.ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_π 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (hS : S.Exact) [CategoryTheory.Limits.HasZeroObject C] (kf : CategoryTheory.Limits.KernelFork S.g) (hkf : CategoryTheory.Limits.IsLimit kf) : (hS.leftHomologyDataOfIsLimitKernelFork kf hkf).π = 0
• CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_ι 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (hS : S.Exact) [CategoryTheory.Limits.HasZeroObject C] (cc : CategoryTheory.Limits.CokernelCofork S.f) (hcc : CategoryTheory.Limits.IsColimit cc) : (hS.rightHomologyDataOfIsColimitCokernelCofork cc hcc).ι = 0
• CategoryTheory.ShortComplex.Splitting.shortExact 📋 Mathlib.Algebra.Homology.ShortComplex.ShortExact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} [CategoryTheory.Limits.HasZeroObject C] (s : S.Splitting) : S.ShortExact
• CategoryTheory.Functor.preservesFiniteColimits_of_preservesCokernels 📋 Mathlib.CategoryTheory.Preadditive.LeftExact
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.HasCoequalizers C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F] : CategoryTheory.Limits.PreservesFiniteColimits F
• CategoryTheory.Functor.preservesFiniteLimits_of_preservesKernels 📋 Mathlib.CategoryTheory.Preadditive.LeftExact
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F] : CategoryTheory.Limits.PreservesFiniteLimits F
• CategoryTheory.Subobject.nontrivial_of_not_isZero 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {X : C} (h : ¬CategoryTheory.Limits.IsZero X) : Nontrivial (CategoryTheory.Subobject X)
• CategoryTheory.MonoOver.botCoeIsoZero 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] {B : C} : ⊥.obj.left ≅ 0
• CategoryTheory.MonoOver.initialTo_b_eq_zero 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {B : C} : CategoryTheory.Limits.initial.to B = 0
• CategoryTheory.Subobject.botCoeIsoZero 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] {B : C} : CategoryTheory.Subobject.underlying.obj ⊥ ≅ 0
• CategoryTheory.Subobject.bot_factors_iff_zero 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {A B : C} (f : A ⟶ B) : ⊥.Factors f ↔ f = 0
• CategoryTheory.Subobject.mk_eq_bot_iff_zero 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : X ⟶ Y} [CategoryTheory.Mono f] : CategoryTheory.Subobject.mk f = ⊥ ↔ f = 0

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