prod_fermatNumber — Mathlib

English

For all natural numbers n, the product of Fermat numbers up to n−1 equals F_n − 2.

Русский

Для всех натуральных n произведение чисел Фермат до n−1 равно F_n − 2.

LaTeX

$$$\\prod_{k=0}^{n-1} \\mathrm{fermatNumber}(k) = \\mathrm{fermatNumber}(n) - 2$$$

Lean4

theorem prod_fermatNumber (n : ℕ) : ∏ k ∈ range n, fermatNumber k = fermatNumber n - 2 := by
  induction n with
  | zero => rfl
  | succ n
    hn =>
    rw [prod_range_succ, hn, fermatNumber, fermatNumber, mul_comm, (show 2 ^ 2 ^ n + 1 - 2 = 2 ^ 2 ^ n - 1 by cutsat), ←
      sq_sub_sq]
    ring_nf
    cutsat

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