noncomputable def ExtGroup {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] (M A : C) (n : ℕ) : Type w

@[implicit_reducible]

noncomputable instance ExtGroup.instAddCommGroup {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] (M A : C) (n : ℕ) : AddCommGroup (ExtGroup M A n)

noncomputable def ExtGroup_R (R : Type u) [Ring R] [Small.{v, u} R] (M A : ModuleCat R) (n : ℕ) : Type v

@[implicit_reducible]

noncomputable instance ExtGroup_R.instAddCommGroup (R : Type u) [Ring R] [Small.{v, u} R] (M A : ModuleCat R) (n : ℕ) : AddCommGroup (ExtGroup_R R M A n)