English
If i ∈ s and, for all j ∈ s with j ≠ i, (f_j).supDegree D < (f_i).supDegree D, then the sum over s has its supremum degree equal to that of f_i and its leading coefficient equal to that of f_i.
Русский
Если i ∈ s и для всех j ∈ s, j ≠ i, (f_j).supDegree D < (f_i).supDegree D, тогда supDegree и leadingCoeff суммы равны тем соответствующим f_i.
LaTeX
$$i ∈ s → (∀ j ∈ s, j ≠ i → (f_j).supDegree D < (f_i).supDegree D) → (∑_{j∈s} f_j).supDegree D = (f_i).supDegree D ∧ (∑_{j∈s} f_j).leadingCoeff D = (f_i).leadingCoeff D$$
Lean4
theorem sum_ne_zero_of_injOn_supDegree' (hs : ∃ i ∈ s, f i ≠ 0) (hd : (s : Set ι).InjOn (supDegree D ∘ f)) :
∑ i ∈ s, f i ≠ 0 := by
obtain ⟨j, hj, hne⟩ := hs
obtain ⟨i, hi, he⟩ := exists_mem_eq_sup _ ⟨j, hj⟩ (supDegree D ∘ f)
by_cases h : ∀ k ∈ s, k = i
· refine (sum_eq_single_of_mem j hj (fun k hk hne => ?_)).trans_ne hne
rw [h k hk, h j hj] at hne; exact hne.irrefl.elim
push_neg at h; obtain ⟨j, hj, hne⟩ := h
apply ne_zero_of_supDegree_ne_bot (D := D)
have (k) (hk : k ∈ s) (hne : k ≠ i) : supDegree D (f k) < supDegree D (f i) :=
((le_sup hk).trans_eq he).lt_of_ne (hd.ne hk hi hne)
rw [(supDegree_leadingCoeff_sum_eq hi this).1]
exact (this j hj hne).ne_bot
