R : Type u_1
inst✝ : Semiring R
k : ℕ
f p : R[X]
n : ℕ
h : natDegree p < n
⊢ ∑ n_1 in support p, ↑(monomial (n_1 - n)) (↑(choose n_1 n) * coeff p n_1) = 0
R : Type u_1
inst✝ : Semiring R
k : ℕ
f p : R[X]
n : ℕ
h : natDegree p < n
⊢ ↑(hasseDeriv n) p = 0
rw [hasseDeriv_apply, sum_def]
R : Type u_1
inst✝ : Semiring R
k : ℕ
f p : R[X]
n : ℕ
h : natDegree p < n
x : ℕ
hx : x ∈ support p
⊢ ↑(monomial (x - n)) (↑(choose x n) * coeff p x) = 0
R : Type u_1
inst✝ : Semiring R
k : ℕ
f p : R[X]
n : ℕ
h : natDegree p < n
⊢ ∑ n_1 in support p, ↑(monomial (n_1 - n)) (↑(choose n_1 n) * coeff p n_1) = 0
refine' Finset.sum_eq_zero fun x hx => _
no goals
R : Type u_1
inst✝ : Semiring R
k : ℕ
f p : R[X]
n : ℕ
h : natDegree p < n
x : ℕ
hx : x ∈ support p
⊢ ↑(monomial (x - n)) (↑(choose x n) * coeff p x) = 0
simp [Nat.choose_eq_zero_of_lt ((le_natDegree_of_mem_supp _ hx).trans_lt h)]