English
For any Hahn series x and natural n, the support of x^n is contained in the additive submonoid generated by the support of x: supp(x^n) ⊆ closure(supp(x)).
Русский
Для любой серии Ганна x и натурального n поддержка x^n содержится в порождающем подгомогеноде добавления опоры x: supp(x^n) ⊆ closure(supp(x)).
LaTeX
$$$\operatorname{supp}(x^n) \subseteq \operatorname{AddSubmonoid.closure}(\operatorname{supp}(x)).$$$
Lean4
theorem support_pow_subset_closure [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R]
(x : HahnSeries Γ R) (n : ℕ) : support (x ^ n) ⊆ AddSubmonoid.closure (support x) :=
by
intro g hn
induction n generalizing g with
| zero =>
simp only [pow_zero, mem_support, coeff_one, ne_eq, ite_eq_right_iff, Classical.not_imp] at hn
simp only [hn, SetLike.mem_coe]
exact AddSubmonoid.zero_mem _
| succ n ih =>
obtain ⟨i, hi, j, hj, rfl⟩ := support_mul_subset_add_support hn
exact SetLike.mem_coe.2 (AddSubmonoid.add_mem _ (ih hi) (AddSubmonoid.subset_closure hj))
