∀ {k G : Type u} [inst : CommRing k] [inst_1 : CommGroup G] [inst_2 : Fintype G] (A : Rep k G) (g : G)
  [inst_3 : DecidableEq G] (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) [inst_4 : NeZero i] (hi : Even i)
  (x y : ↥(LinearMap.ker A.ρ.norm)),
  (CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupHomologyπEven A g hg i hi)) x =
      (CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupHomologyπEven A g hg i hi)) y ↔
    ↑x - ↑y ∈ (ModuleCat.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A).hom).range