English
Let α be a commutative semiring and s ⊆ α with span(s) = ⊤. Then for every n ∈ ℕ, span({ x^n : x ∈ s }) = ⊤.
Русский
Пусть α — коммутативное полукольцо, и S — подмножество α такое, что span(S) = ⊤. Тогда для каждого n ∈ ℕ мощность x^n порождает ⊤: span({ x^n : x ∈ S }) = ⊤.
LaTeX
$$$\\operatorname{span}(s)=\\top \\Rightarrow \\forall n \\in \\mathbb{N},\\ \\operatorname{span}\\bigl(\\{x^n : x \\in s\\}\\bigr)=\\top$$$
Lean4
theorem span_pow_eq_top (s : Set α) (hs : span s = ⊤) (n : ℕ) : span ((fun (x : α) => x ^ n) '' s) = ⊤ :=
by
rw [eq_top_iff_one]
rcases n with - | n
· obtain rfl | ⟨x, hx⟩ := eq_empty_or_nonempty s
· rw [Set.image_empty, hs]
trivial
· exact subset_span ⟨_, hx, pow_zero _⟩
rw [eq_top_iff_one, span, Finsupp.mem_span_iff_linearCombination] at hs
rcases hs with ⟨f, hf⟩
simp only [Finsupp.linearCombination, Finsupp.coe_lsum, Finsupp.sum, LinearMap.coe_smulRight, LinearMap.id_coe, id_eq,
smul_eq_mul] at hf
have := sum_pow_mem_span_pow f.support (fun a => f a * a) n
rw [hf, one_pow] at this
refine span_le.mpr ?_ this
rintro _ hx
simp_rw [Set.mem_image] at hx
rcases hx with ⟨x, _, rfl⟩
have : span ({(x : α) ^ (n + 1)} : Set α) ≤ span ((fun x : α => x ^ (n + 1)) '' s) :=
by
rw [span_le, Set.singleton_subset_iff]
exact subset_span ⟨x, x.prop, rfl⟩
refine this ?_
rw [mul_pow, mem_span_singleton]
exact ⟨f x ^ (n + 1), mul_comm _ _⟩
