Mathlib Map

Theorems · Theorem · category theory

CategoryTheory.HasExt.standard

∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C], CategoryTheory.HasExt C
Defined in
Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Cited by
22 results in Mathlib
Foundations
Depth 108 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CategoryTheory.CategoryCategoryTheory.Abelian
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

CategoryTheory.HasProjectiveDimensionLT.subsingleton · cited by 3HasProjectiveDimensionLT.…CategoryTheory.projective_iff_hasProjectiveDimensionLT_one · cited by 3CategoryTheory.projective…CategoryTheory.HasProjectiveDimensionLT.mk · cited by 2HasProjectiveDimensionLT.…CategoryTheory.HasInjectiveDimensionLT.mk · cited by 2HasInjectiveDimensionLT.mkCategoryTheory.HasInjectiveDimensionLT.subsingleton · cited by 2HasInjectiveDimensionLT.s…CategoryTheory.hasProjectiveDimensionLT_of_ge · cited by 2CategoryTheory.hasProject…CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_X₃ · cited by 2ShortExact.hasProjectiveD…CategoryTheory.Retract.hasInjectiveDimensionLT · cited by 2Retract.hasInjectiveDimen…CategoryTheory.Retract.hasProjectiveDimensionLT · cited by 2Retract.hasProjectiveDime…CategoryTheory.Limits.IsZero.hasProjectiveDimensionLT_zero · cited by 2IsZero.hasProjectiveDimen…CategoryTheory.HasProjectiveDimensionLT.subsingleton' · cited by 1HasProjectiveDimensionLT.…CategoryTheory.hasInjectiveDimensionLT_of_ge · cited by 1CategoryTheory.hasInjecti…CategoryTheory.isZero_of_hasInjectiveDimensionLT_zero · cited by 1CategoryTheory.isZero_of_…CategoryTheory.isZero_of_hasProjectiveDimensionLT_zero · cited by 1CategoryTheory.isZero_of_…CategoryTheory.HasInjectiveDimensionLT.subsingleton' · cited by 1HasInjectiveDimensionLT.s…CategoryTheory.Category · cited by 32673CategoryTheory.CategoryCategoryTheory.Abelian · cited by 1753CategoryTheory.AbelianCategoryTheory.HasExt · cited by 218CategoryTheory.HasExtHasDerivedCategory · cited by 190HasDerivedCategoryHasDerivedCategory.standard · cited by 42HasDerivedCategory.standa…CategoryTheory.hasExt_of_hasDerivedCategory · cited by 3CategoryTheory.hasExt_of_…HasExt.standardCITED BYCITES

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by26

Results whose statement or proof uses this declaration.