English
The derivative of the Bernoulli polynomial B_{k+1} equals (k+1) B_k.
Русский
Производная полинома Бернулли B_{k+1} равна (k+1) B_k.
LaTeX
$$Polynomial.derivative(bernoulli(k+1)) = (k+1) · bernoulli(k)$$
Lean4
theorem derivative_bernoulli_add_one (k : ℕ) : Polynomial.derivative (bernoulli (k + 1)) = (k + 1) * bernoulli k :=
by
simp_rw [bernoulli, derivative_sum, derivative_monomial, Nat.sub_sub, Nat.add_sub_add_right]
-- LHS sum has an extra term, but the coefficient is zero:
rw [range_add_one, sum_insert notMem_range_self, tsub_self, cast_zero, mul_zero, map_zero, zero_add, mul_sum]
-- the rest of the sum is termwise equal:
refine sum_congr (by rfl) fun m _ => ?_
conv_rhs => rw [← Nat.cast_one, ← Nat.cast_add, ← C_eq_natCast, C_mul_monomial, mul_comm]
rw [mul_assoc, mul_assoc, ← Nat.cast_mul, ← Nat.cast_mul]
congr 3
rw [(choose_mul_succ_eq k m).symm]
