A : Type ?u.633621
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ bernoulli 1 = -(1 / 2)
A : Type ?u.633621
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ bernoulli 1 = -1 / 2
norm_num
no goals
A : Type ?u.633621
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ bernoulli 1 = -(1 / 2)
simp [bernoulli]