English
There exists an integral combination f with support in b.support such that P.root i equals the sum ∑ j ∈ b.support f j • P.root j.
Русский
Существует целочисленная комбинация f, опора которой в b.support, такая что P.root i = ∑ j ∈ b.support f j • P.root j.
LaTeX
$$exists_root_eq_sum_int (P := P) (b := b) i$$
Lean4
theorem exists_root_eq_sum_int [CharZero R] (i : ι) :
∃ f : ι → ℤ, f.support ⊆ b.support ∧ (0 < f ∨ f < 0) ∧ P.root i = ∑ j ∈ b.support, f j • P.root j :=
by
obtain ⟨f, hf, hf' | hf'⟩ := b.exists_root_eq_sum_nat_or_neg i
· refine ⟨Nat.cast ∘ f, by simpa, Or.inl <| Pi.lt_def.mpr ⟨fun _ ↦ by simp, ?_⟩, by simp [hf']⟩
by_contra! contra
replace contra : f = 0 := by ext i; simpa using contra i
exact P.ne_zero i <| by simp [hf', contra]
· refine ⟨-Nat.cast ∘ f, by simpa, Or.inr <| Pi.lt_def.mpr ⟨fun _ ↦ by simp, ?_⟩, by simp [hf']⟩
by_contra! contra
replace contra : f = 0 := by ext i; simpa using contra i
exact P.ne_zero i <| by simp [hf', contra]
