English
Under the same hypotheses as above, if p.supDegree D = q.supDegree D and p.leadingCoeff D = q.leadingCoeff D, then (p - q).supDegree D < p.supDegree D ∨ p = q.
Русский
При тех же условиях, если степени равны и ведущие коэффициенты равны, то (p - q).supDegree D < p.supDegree D или p = q.
LaTeX
$$$(p - q).supDegree D < p.supDegree D \lor p = q$$$
Lean4
theorem supDegree_leadingCoeff_sum_eq (hi : i ∈ s) (hmax : ∀ 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 := by
classical
rw [← s.add_sum_erase _ hi]
by_cases hs : s.erase i = ∅
· rw [hs, Finset.sum_empty, add_zero]; exact ⟨rfl, rfl⟩
suffices _ from ⟨supDegree_add_eq_left this, leadingCoeff_add_eq_left this⟩
refine supDegree_sum_lt ?_ (fun j hj => ?_)
· rw [Finset.nonempty_iff_ne_empty]; exact hs
· rw [Finset.mem_erase] at hj; exact hmax j hj.2 hj.1
