isZero_Ext_succ_of_projective

theorem isZero_Ext_succ_of_projective : ∀ {R : Type u_1} [inst : Ring R] {C : Type u_2} [inst_1 : CategoryTheory.Category.{u_3, u_2} C] [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.Linear R C] [inst_4 : CategoryTheory.EnoughProjectives C] (X Y : C) [inst_5 : CategoryTheory.Projective X] (n : ℕ), CategoryTheory.Limits.IsZero (((Ext R C (n + 1)).obj (Opposite.op X)).obj Y)

The theorem `isZero_Ext_succ_of_projective` states that for a ring `R`, a category `C` that is abelian, linear over `R`, and has enough projectives, if `X` is a projective object in `C` and `n` is a natural number, then the `(n + 1)`-th Ext functor applied to `X` and any object `Y` in the category `C` results in a zero object. In the context of homological algebra, this means that higher extensions of projective objects are always zero.

More concisely: In an abelian, linear category with enough projectives over a ring, the $(n+1)$-th Ext functor of a projective object with any object is zero for all natural numbers $n$.