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 ∈ 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 ∈ 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 ∈ 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 ∈ closure (Set.range f)) : ∃ (a : ι → ℕ), x = ∑ i : ι, a i • f i

theorem Submonoid.mem_closure_range_iff {M : Type u_1} [CommMonoid M] {ι : Type u_2} {f : ι → M} {x : M} : x ∈ 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 ∈ closure (Set.range f) ↔ ∃ (a : ι →₀ ℕ), x = a.sum fun (x1 : ι) (x2 : ℕ) => x2 • f x1

theorem Submonoid.mem_closure_range_iff_of_fintype {M : Type u_1} [CommMonoid M] {ι : Type u_2} {f : ι → M} {x : M} [Fintype ι] : x ∈ 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 ∈ closure (Set.range f) ↔ ∃ (a : ι → ℕ), x = ∑ i : ι, a i • f i

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

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

theorem Submonoid.mem_closure_finset' {M : Type u_1} [CommMonoid M] {x : M} {s : Finset M} : x ∈ closure ↑s ↔ ∃ (a : { x : M // x ∈ s } → ℕ), x = ∏ i : { x : M // x ∈ s }, ↑i ^ a i

A variant of Submonoid.mem_closure_finset using s as the index type.

theorem AddSubmonoid.mem_closure_finset' {M : Type u_1} [AddCommMonoid M] {x : M} {s : Finset M} : x ∈ closure ↑s ↔ ∃ (a : { x : M // x ∈ s } → ℕ), x = ∑ i : { x : M // x ∈ s }, a i • ↑i

A variant of AddSubmonoid.mem_closure_finset using s as the index type.