supDegree_add_eq_left — Mathlib

English

If p and q satisfy certain degree bounds at ap and aq respectively, then the coefficient of p*q at ap+aq equals the product of the coefficients at ap and aq.

Русский

При заданных степенных границах коэффициент произведения в ap+aq равен произведению коэффициентов в ap и aq.

LaTeX

$$$(p * q)(ap + aq) = p(ap) \cdot q(aq)$$

Lean4

theorem supDegree_add_eq_left (h : q.supDegree D < p.supDegree D) : (p + q).supDegree D = p.supDegree D :=
  by
  apply (supDegree_add_le.trans <| sup_le le_rfl h.le).antisymm
  obtain ⟨a, ha, he⟩ := exists_supDegree_mem_support D (ne_zero_of_not_supDegree_le h.not_ge)
  rw [he] at h ⊢
  apply Finset.le_sup
  rw [mem_support_iff, add_apply, apply_eq_zero_of_not_le_supDegree h.not_ge, add_zero]
  exact mem_support_iff.mp ha

Похожие утверждения