coeff_eq_zero_of_lt — Mathlib

English

If the degree of f is strictly less than a monomial d in the MonomialOrder m, then the coefficient of d in f is zero.

Русский

Если степень f строго меньше данного монома d по порядку m, то коэффициент при d в f равен нулю.

LaTeX

$$$\text{If } m.\mathrm{degree}(f) \prec_m d\text{ then } f_d = 0$$$

Lean4

theorem coeff_eq_zero_of_lt {f : MvPolynomial σ R} {d : σ →₀ ℕ} (hd : m.degree f ≺[m] d) : f.coeff d = 0 :=
  by
  rw [← not_le] at hd
  by_contra hf
  apply hd (m.le_degree (mem_support_iff.mpr hf))

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