∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep k G} (x : G × G →₀ ↑A.V),
  (x ∈ groupHomology.cycles₂ A) =
    ((x.sum fun g a => (fun₀ | g.2 => (A.ρ g.1⁻¹) a) + fun₀ | g.1 => a) = x.sum fun g a => fun₀ | g.1 * g.2 => a)