Low-degree group cohomology compatibility

This file restores upstream aliases and multiplicative cocycle closure lemmas.

theorem groupCohomology.IsMulCocycle₂.of_mem_cocycles₂ {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] (f : G × G → M) (hf : f ∈ cocycles₂ (Rep.ofMulDistribMulAction G M)) : IsMulCocycle₂ (⇑Additive.toMul ∘ f)

Alias of groupCohomology.isMulCocycle₂_of_mem_cocycles₂.

theorem groupCohomology.IsMulCocycle₂.mul {G : Type u_1} {M : Type u_2} [Group G] [CommGroup M] [MulDistribMulAction G M] {f g : G × G → M} (hf : IsMulCocycle₂ f) (hg : IsMulCocycle₂ g) : IsMulCocycle₂ (f * g)

instance instFactIsMulCocycle₂HMulForallProd_leanPool {G : Type u_1} {M : Type u_2} [Group G] [CommGroup M] [MulDistribMulAction G M] {f g : G × G → M} [Fact (groupCohomology.IsMulCocycle₂ f)] [Fact (groupCohomology.IsMulCocycle₂ g)] : Fact (groupCohomology.IsMulCocycle₂ (f * g))