mersenne_mod_three — Mathlib

English

If n is odd and at least 3, then M_n ≡ 1 (mod 3).

Русский

Если n нечетно и n ≥ 3, то M_n ≡ 1 (mod 3).

LaTeX

$$If $n$ is odd and $n \ge 3$, then $mersenne\ n \equiv 1 \pmod{3}$$$

Lean4

theorem mersenne_mod_three {n : ℕ} (odd : Odd n) (h : 3 ≤ n) : mersenne n % 3 = 1 :=
  by
  obtain ⟨k, rfl⟩ := odd
  replace h : 1 ≤ k := by omega
  induction k, h using Nat.le_induction with
  | base => rfl
  | succ j _ _ =>
    rw [mersenne_succ, show 2 * (j + 1) = 2 * j + 1 + 1 by cutsat, mersenne_succ]
    cutsat

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