no goals
A : Type ?u.151020
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ bernoulli' n = 1 - ∑ k in range n, ↑(Nat.choose n k) / (↑n - ↑k + 1) * bernoulli' k
rw [bernoulli'_def', ← Fin.sum_univ_eq_sum_range]