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