English
Let p, q be polynomials over a semiring R. If the sum of their leading coefficients is nonzero, then the degree of p + q equals the maximum of the degrees of p and q: deg(p+q) = max(deg p, deg q).
Русский
Пусть p и q — полиномы над полупрямой R. Если сумма ведущих коэффициентов не равна нулю, то deg(p+q) = max(deg p, deg q).
LaTeX
$$$\deg(p + q) = \max(\deg p, \deg q) \quad$ при $\operatorname{leadingCoeff}(p) + \operatorname{leadingCoeff}(q) \neq 0$$$
Lean4
theorem degree_add_eq_of_leadingCoeff_add_ne_zero (h : leadingCoeff p + leadingCoeff q ≠ 0) :
degree (p + q) = max p.degree q.degree :=
le_antisymm (degree_add_le _ _) <|
match lt_trichotomy (degree p) (degree q) with
| Or.inl hlt => by rw [degree_add_eq_right_of_degree_lt hlt, max_eq_right_of_lt hlt]
| Or.inr (Or.inl HEq) =>
le_of_not_gt fun hlt : max (degree p) (degree q) > degree (p + q) =>
h <|
show leadingCoeff p + leadingCoeff q = 0 by
rw [HEq, max_self] at hlt
rw [leadingCoeff, leadingCoeff, natDegree_eq_of_degree_eq HEq, ← coeff_add]
exact coeff_natDegree_eq_zero_of_degree_lt hlt
| Or.inr (Or.inr hlt) => by rw [degree_add_eq_left_of_degree_lt hlt, max_eq_left_of_lt hlt]
