coeff_natDegree_succ_eq_zero — Mathlib

English

Coefficent at natDegree(p) + 1 is zero: coeff(p, natDegree(p) + 1) = 0.

Русский

Коэффициент при степени natDegree(p) + 1 равен нулю.

LaTeX

$$$ p \in R[X] \Rightarrow p.coeff(p.natDegree + 1) = 0 $$$

Lean4

@[simp]
theorem coeff_natDegree_succ_eq_zero {p : R[X]} : p.coeff (p.natDegree + 1) = 0 :=
  coeff_eq_zero_of_natDegree_lt
    (lt_add_one _)
      -- We need the explicit `Decidable` argument here because an exotic one shows up in a moment!

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