Powers of homological complex endomorphisms

Degreewise recursion for powers of a complex endomorphism. This only needs a category with zero morphisms, so it is available independently of additive structure and chain homotopies.

theorem HomologicalComplex.pow_f_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_1} {c : ComplexShape ι} {K : HomologicalComplex C c} {s : K ⟶ K} (m : ℕ) (i : ι) : (CategoryTheory.End.of s ^ (m + 1)).f i = CategoryTheory.CategoryStruct.comp ((CategoryTheory.End.of s ^ m).f i) (s.f i)

Degreewise recursion for the powers of a chain endomorphism.