English
If a ≼ deg f and b ≼ deg g, then the coefficient of a+b in f·g equals the product of coefficients at a and b.
Русский
Если a ≤ deg f и b ≤ deg g, то коэффициент при a+b в f·g равен произведению коэффициентов при a и b.
LaTeX
$$$f,g:\; (a,b) \in ? \Rightarrow f.\mathrm{coeff}(a) \cdot g.\mathrm{coeff}(b) = (f*g).\mathrm{coeff}(a+b)$$$
Lean4
/-- Multiplicativity of leading coefficients -/
theorem coeff_mul_of_add_of_degree_le {f g : MvPolynomial σ R} {a b : σ →₀ ℕ} (ha : m.degree f ≼[m] a)
(hb : m.degree g ≼[m] b) : (f * g).coeff (a + b) = f.coeff a * g.coeff b := by
classical
rw [coeff_mul, Finset.sum_eq_single (a, b)]
· rintro ⟨c, d⟩ hcd h
simp only [Finset.mem_antidiagonal] at hcd
by_cases hf : m.degree f ≺[m] c
· rw [m.coeff_eq_zero_of_lt hf, zero_mul]
· suffices m.degree g ≺[m] d by rw [coeff_eq_zero_of_lt this, mul_zero]
rw [not_lt] at hf
rw [← not_le]
intro hf'
apply h
suffices c = a by simpa [Prod.mk.injEq, this] using hcd
apply m.toSyn.injective
apply le_antisymm (le_trans hf ha)
apply le_of_add_le_add_right (a := m.toSyn b)
rw [← map_add, ← hcd, map_add]
simp only [add_le_add_iff_left]
exact le_trans hf' hb
· simp
