hasseDeriv_eq_zero_of_lt_natDegree

English

If the natDegree of p is less than n, then the n-th Hasse derivative is zero.

Русский

Если NAT-степень p меньше n, то n-я производная Хассе равна нулю.

LaTeX

$$$\operatorname{natDegree}(p) < n \implies \mathrm{hasseDeriv}_n(p) = 0$$$

Lean4

theorem hasseDeriv_eq_zero_of_lt_natDegree (p : R[X]) (n : ℕ) (h : p.natDegree < n) : hasseDeriv n p = 0 :=
  by
  rw [hasseDeriv_apply, sum_def]
  refine Finset.sum_eq_zero fun x hx => ?_
  simp [Nat.choose_eq_zero_of_lt ((le_natDegree_of_mem_supp _ hx).trans_lt h)]

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