bernoulli_eq_bernoulli'_of_ne_one

English

If n ≠ 1, then Bernoulli number equals Bernoulli' number.

Русский

Если n ≠ 1, то B_n = B'_n.

LaTeX

$$$\forall n \in \mathbb{N},\; n \neq 1 \Rightarrow bernoulli n = bernoulli' n$$$

Lean4

theorem bernoulli_eq_bernoulli'_of_ne_one {n : ℕ} (hn : n ≠ 1) : bernoulli n = bernoulli' n :=
  by
  by_cases h0 : n = 0; · simp [h0]
  rw [bernoulli, neg_one_pow_eq_pow_mod_two]
  rcases mod_two_eq_zero_or_one n with h | h
  · simp [h]
  · simp [bernoulli'_odd_eq_zero (odd_iff.mpr h) (one_lt_iff_ne_zero_and_ne_one.mpr ⟨h0, hn⟩)]

Похожие утверждения