coeff_natTrailingDegree_pred_eq_zero

English

If natTrailingDegree(p) > 0, then p.coeff (natTrailingDegree(p) - 1) = 0.

Русский

Если natTrailingDegree(p) > 0, то p.coeff(natTrailingDegree(p) - 1) = 0.

LaTeX

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

Lean4

@[simp]
theorem coeff_natTrailingDegree_pred_eq_zero {p : R[X]} {hp : (0 : ℕ∞) < natTrailingDegree p} :
    p.coeff (p.natTrailingDegree - 1) = 0 :=
  coeff_eq_zero_of_lt_natTrailingDegree <| Nat.sub_lt (WithTop.coe_pos.mp hp) Nat.one_pos

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