theorem mapRange_linearMap_add_apply {k : Type u} [CommRing k] {α M N : Type u} [AddCommGroup M] [Module k M] [AddCommGroup N] [Module k N] (f g : M →ₗ[k] N) (x : α →₀ M) : (Finsupp.mapRange.linearMap (f + g)) x = (Finsupp.mapRange.linearMap f) x + (Finsupp.mapRange.linearMap g) x

instance chainsFunctor_additive (k G : Type u) [CommRing k] [Group G] : (groupHomology.chainsFunctor k G).Additive

noncomputable def homology_biprod_iso (k G : Type u) [CommRing k] [Group G] (A B : Rep k G) (n : ℕ) : groupHomology (A ⊞ B) n ≅ groupHomology A n ⊞ groupHomology B n