theorem GroupCohomology.homology_induced_vanishing {k : Type u} [CommRing k] {G : Type u} [Group G] [DecidableEq G] (A : Rep.{u, u, u} k ↥⊥) (n : ℕ) : CategoryTheory.Limits.IsZero (groupHomology (Rep.ind ⊥.subtype A) (n + 1))

noncomputable def GroupCohomology.homology_induced_H0_iso {k : Type u} [CommRing k] {G : Type u} [Group G] [DecidableEq G] (A : Rep.{u, u, u} k ↥⊥) : groupHomology (Rep.ind ⊥.subtype A) 0 ≅ groupHomology A 0