apply_eq_zero_of_not_le_supDegree

English

If a coefficient p(a) of a monomial is zero whenever its degree is not large enough to cover a given D a, then p(a)=0.

Русский

Если коэффициент полинома равен нулю там, где степень не достигает значения D(a), то p(a)=0.

LaTeX

$$$\\neg (D a \\le p.supDegree D) \\Rightarrow p a = 0$$$

Lean4

theorem apply_eq_zero_of_not_le_supDegree {p : R[A]} {a : A} (hlt : ¬D a ≤ p.supDegree D) : p a = 0 :=
  by
  contrapose! hlt
  exact Finset.le_sup (Finsupp.mem_support_iff.2 hlt)

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