Connection between Subgroup.closure and Finsupp.prod

theorem Subgroup.exists_finsupp_of_mem_closure_range {M : Type u_1} [CommGroup M] {ι : Type u_2} (f : ι → M) (x : M) (hx : x ∈ closure (Set.range f)) : ∃ (a : ι →₀ ℤ), x = a.prod fun (x1 : ι) (x2 : ℤ) => f x1 ^ x2

theorem AddSubgroup.exists_finsupp_of_mem_closure_range {M : Type u_1} [AddCommGroup M] {ι : Type u_2} (f : ι → M) (x : M) (hx : x ∈ closure (Set.range f)) : ∃ (a : ι →₀ ℤ), x = a.sum fun (x1 : ι) (x2 : ℤ) => x2 • f x1

theorem Subgroup.exists_of_mem_closure_range {M : Type u_1} [CommGroup M] {ι : Type u_2} (f : ι → M) (x : M) [Fintype ι] (hx : x ∈ closure (Set.range f)) : ∃ (a : ι → ℤ), x = ∏ i : ι, f i ^ a i

theorem AddSubgroup.exists_of_mem_closure_range {M : Type u_1} [AddCommGroup M] {ι : Type u_2} (f : ι → M) (x : M) [Fintype ι] (hx : x ∈ closure (Set.range f)) : ∃ (a : ι → ℤ), x = ∑ i : ι, a i • f i

theorem Subgroup.mem_closure_range_iff {M : Type u_1} [CommGroup M] {ι : Type u_2} {f : ι → M} {x : M} : x ∈ closure (Set.range f) ↔ ∃ (a : ι →₀ ℤ), x = a.prod fun (x1 : ι) (x2 : ℤ) => f x1 ^ x2

theorem AddSubgroup.mem_closure_range_iff {M : Type u_1} [AddCommGroup M] {ι : Type u_2} {f : ι → M} {x : M} : x ∈ closure (Set.range f) ↔ ∃ (a : ι →₀ ℤ), x = a.sum fun (x1 : ι) (x2 : ℤ) => x2 • f x1

theorem Subgroup.mem_closure_range_iff_of_fintype {M : Type u_1} [CommGroup M] {ι : Type u_2} {f : ι → M} {x : M} [Fintype ι] : x ∈ closure (Set.range f) ↔ ∃ (a : ι → ℤ), x = ∏ i : ι, f i ^ a i

theorem AddSubgroup.mem_closure_range_iff_of_fintype {M : Type u_1} [AddCommGroup M] {ι : Type u_2} {f : ι → M} {x : M} [Fintype ι] : x ∈ closure (Set.range f) ↔ ∃ (a : ι → ℤ), x = ∑ i : ι, a i • f i

theorem Subgroup.mem_closure_iff_of_fintype {M : Type u_1} [CommGroup M] {x : M} {s : Set M} [Fintype ↑s] : x ∈ closure s ↔ ∃ (a : ↑s → ℤ), x = ∏ i : ↑s, ↑i ^ a i

theorem AddSubgroup.mem_closure_iff_of_fintype {M : Type u_1} [AddCommGroup M] {x : M} {s : Set M} [Fintype ↑s] : x ∈ closure s ↔ ∃ (a : ↑s → ℤ), x = ∑ i : ↑s, a i • ↑i