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