English
Let f: S → R[X] and s be a Finset S such that the nonzero terms f(i) have pairwise disjoint degrees. Then the degree of the sum equals the supremum of the degrees of the summands.
Русский
Пусть f: S → R[X] и s — конечное множество S так, что ненулевые элементы f(i) имеют попарно непересекающиеся степени. Тогда deg(∑_{i∈s} f(i)) равен максимуму степеней (supremum) по i∈s.
LaTeX
$$$\deg\Big(\sum_{i\in s} f(i)\Big) = \sup_{i\in s} \deg(f(i))$$$
Lean4
theorem degree_sum_eq_of_disjoint (f : S → R[X]) (s : Finset S)
(h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f)) : degree (s.sum f) = s.sup fun i => degree (f i) := by
classical
induction s using Finset.induction_on with
| empty => simp
| insert x s hx IH =>
simp only [hx, Finset.sum_insert, not_false_iff, Finset.sup_insert]
specialize IH (h.mono fun _ => by simp +contextual)
rcases lt_trichotomy (degree (f x)) (degree (s.sum f)) with (H | H | H)
· rw [← IH, sup_eq_right.mpr H.le, degree_add_eq_right_of_degree_lt H]
· rcases s.eq_empty_or_nonempty with (rfl | hs)
· simp
obtain ⟨y, hy, hy'⟩ := Finset.exists_mem_eq_sup s hs fun i => degree (f i)
rw [IH, hy'] at H
by_cases hx0 : f x = 0
· simp [hx0, IH]
have hy0 : f y ≠ 0 := by
contrapose! H
simpa [H, degree_eq_bot] using hx0
refine absurd H (h ?_ ?_ fun H => hx ?_)
· simp [hx0]
· simp [hy, hy0]
· exact H.symm ▸ hy
· rw [← IH, sup_eq_left.mpr H.le, degree_add_eq_left_of_degree_lt H]
