Transport of bounded independence through injective homomorphisms

theorem Wallace.FiniteCombinatorics.boundedIndependent_of_image {G : Type u} {H : Type v} [AddCommGroup G] [AddCommGroup H] [DecidableEq H] (f : G →+ H) (hf : Function.Injective ⇑f) {M : ℕ} {X : Finset G} (himage : BoundedIndependent M (Finset.image (⇑f) X)) : BoundedIndependent M X

Bounded independence is reflected by an injective additive homomorphism.