English
The degree of a product is bounded above by the sum of the degrees: deg(fg) ≼_m deg f + deg g.
Русский
Степень произведения не превосходит суммы степеней: deg(fg) ≼_m deg f + deg g.
LaTeX
$$$m.degree (f*g) \preceq_m m.degree f + m.degree g$$$
Lean4
theorem degree_mul_le {f g : MvPolynomial σ R} : m.degree (f * g) ≼[m] m.degree f + m.degree g := by
classical
rw [degree_le_iff]
intro c
rw [← not_lt, mem_support_iff, not_imp_not]
intro hc
rw [coeff_mul]
apply Finset.sum_eq_zero
rintro ⟨d, e⟩ hde
simp only [Finset.mem_antidiagonal] at hde
dsimp only
by_cases hd : m.degree f ≺[m] d
· rw [m.coeff_eq_zero_of_lt hd, zero_mul]
· suffices m.degree g ≺[m] e by rw [m.coeff_eq_zero_of_lt this, mul_zero]
simp only [not_lt] at hd
apply lt_of_add_lt_add_left (a := m.toSyn d)
simp only [← map_add, hde]
apply lt_of_le_of_lt _ hc
simp only [map_add]
exact add_le_add_right hd _
