coeff_eq_zero_of_lt_natTrailingDegree

English

If n < p.natTrailingDegree, then p.coeff n = 0.

Русский

Если n < natTrailingDegree(p), то p.coeff n = 0.

LaTeX

$$$n < \operatorname{natTrailingDegree}(p) \Rightarrow p.\text{coeff}(n) = 0$$$

Lean4

theorem coeff_eq_zero_of_lt_natTrailingDegree {p : R[X]} {n : ℕ} (h : n < p.natTrailingDegree) : p.coeff n = 0 :=
  by
  apply coeff_eq_zero_of_lt_trailingDegree
  by_cases hp : p = 0
  · rw [hp, trailingDegree_zero]
    exact WithTop.coe_lt_top n
  · rw [trailingDegree_eq_natTrailingDegree hp]
    exact WithTop.coe_lt_coe.2 h

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