fermatNumber_eq_prod_add_two — Mathlib

English

For all n, F_n equals the product of earlier Fermat numbers plus 2.

Русский

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

LaTeX

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

Lean4

theorem fermatNumber_eq_prod_add_two (n : ℕ) : fermatNumber n = ∏ k ∈ range n, fermatNumber k + 2 :=
  by
  rw [prod_fermatNumber, Nat.sub_add_cancel]
  exact le_of_lt <| two_lt_fermatNumber _

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