@[reducible]

def CategoryTheory.hasLocalEndRings_of_fitting (k : Type w) [Field k] (C : Type u) [Category.{v, u} C] [Abelian C] [Linear k C] [inst : FiniteAbelianCategory.HasLocalEndOfIndecomposable k C] (h_indecomp : ∀ (P : C) [Projective P], Indecomposable P) : HasLocalEndomorphismRings C

Derives the HasLocalEndomorphismRings structure on C from the Fitting-lemma hypothesis that endomorphism rings of indecomposable objects are local, together with the assumption that every projective object is indecomposable.

@[reducible]

def CategoryTheory.hasProjectiveCoversOfSimples_of_fitting (k : Type w) [Field k] (C : Type u) [Category.{v, u} C] [Abelian C] [Linear k C] [FiniteAbelianCategory.HasLocalEndOfIndecomposable k C] (h_indecomp : ∀ (P : C) [Projective P], Indecomposable P) : HasProjectiveCoversOfSimples C

Derives the existence of projective covers of simple objects from the Fitting-lemma hypothesis on local endomorphism rings of indecomposable projectives.