Connection between Submonoid.closure and Finsupp.prod

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

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

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

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

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

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

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

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