English
Let M be a commutative group and f: ι → M a family of elements. If x lies in the closure of the subgroup generated by {f(i) : i ∈ ι}, then x can be written as a finite product x = ∏_{i ∈ ι} f(i)^{a(i)} with integers a(i) and only finitely many a(i) nonzero.
Русский
Пусть M — коммутативная группа и задано семейство элементов f(i). Если x принадлежит замыканию подгруппы, порождённой {f(i)}, то x может быть записано как конечный произведение x = ∏ f(i)^{a(i)} с целыми a(i) и конечной опорой nonzero.
LaTeX
$$$\exists a \in \mathbb{Z}^{(\iota)},\; x = \prod_{i \in \iota} f(i)^{a_i}$$$
Lean4
@[to_additive]
theorem exists_finsupp_of_mem_closure_range (hx : x ∈ closure (Set.range f)) : ∃ a : ι →₀ ℤ, x = a.prod (f · ^ ·) := by
classical
induction hx using closure_induction with
| mem x h => obtain ⟨i, rfl⟩ := h; exact ⟨Finsupp.single i 1, by simp⟩
| one => use 0; simp
| mul x y hx hy hx' hy' =>
obtain ⟨⟨v, rfl⟩, w, rfl⟩ := And.intro hx' hy'
use v + w
rw [Finsupp.prod_add_index]
· simp
· simp [zpow_add]
| inv x hx hx' =>
obtain ⟨a, rfl⟩ := hx'
use -a
rw [Finsupp.prod_neg_index]
· simp
· simp
