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 ↥⊥)
: