natDegree_lt_coeff_mul — Mathlib

English

Let p and q be polynomials over a semiring R, and m,n be natural numbers. If natDegree(p) + natDegree(q) < m + n, then the coefficient of x^(m+n) in p q is 0.

Русский

Пусть p и q — многочлены над полем (или кольцом) R, и m,n ∈ ℕ. Если natDegree(p) + natDegree(q) < m + n, то коэффициент при x^(m+n) в произведении p q равен 0.

LaTeX

$$$\operatorname{natDegree}(p) + \operatorname{natDegree}(q) < m + n \Rightarrow (p q).\coeff(m+n) = 0$$$

Lean4

theorem natDegree_lt_coeff_mul (h : p.natDegree + q.natDegree < m + n) : (p * q).coeff (m + n) = 0 :=
  coeff_eq_zero_of_natDegree_lt (natDegree_mul_le.trans_lt h)

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