English
There exists an integer-valued combination f: ι → ℤ with finite support in b.support such that P.root i equals the sum ∑ j ∈ b.support f j • P.root j or its negation.
Русский
Существует целочисленная комбинация f: ι → ℤ с конечной опорой в b.support так, что P.root i равен сумме ∑ f j • P.root j или её противоположности.
LaTeX
$$∃ f : ι → ℤ, f.support ⊆ b.support ∧ (P.root i = ∑ j ∈ b.support, f j • P.root j ∨ P.root i = -∑ j ∈ b.support, f j • P.root j)$$
Lean4
theorem exists_root_eq_sum_nat_or_neg (i : ι) :
∃ f : ι → ℕ,
f.support ⊆ b.support ∧
(P.root i = ∑ j ∈ b.support, f j • P.root j ∨ P.root i = -∑ j ∈ b.support, f j • P.root j) :=
by
classical
simp_rw [← neg_eq_iff_eq_neg]
suffices
∀ m ∈ AddSubmonoid.closure (P.root '' b.support),
∃ f : ι → ℕ, f.support ⊆ b.support ∧ m = ∑ j ∈ b.support, f j • P.root j
by
rcases b.root_mem_or_neg_mem i with hi | hi
· obtain ⟨f, hf, hf'⟩ := this _ hi
exact ⟨f, hf, Or.inl hf'⟩
· obtain ⟨f, hf, hf'⟩ := this _ hi
exact ⟨f, hf, Or.inr hf'⟩
intro m hm
refine AddSubmonoid.closure_induction ?_ ⟨0, by simp⟩ ?_ hm
· rintro - ⟨j, hj, rfl⟩
exact ⟨Pi.single j 1, by simpa, by aesop (add simp Pi.single_apply)⟩
· intro _ _ _ _ ⟨f, hf, hf'⟩ ⟨g, hg, hg'⟩
refine ⟨f + g, ?_, by simp [hf', hg', add_smul, Finset.sum_add_distrib]⟩
exact (support_add f g).trans <| union_subset_iff.mpr ⟨hf, hg⟩
