fib_coprime_fib_succ — Mathlib

English

For all n, fib(n) and fib(n+1) are coprime: gcd(fib(n), fib(n+1)) = 1.

Русский

Для любого n числа fib(n) и fib(n+1) взаимно просты: gcd(fib(n), fib(n+1)) = 1.

LaTeX

$$gcd(fib(n), fib(n+1)) = 1$$

Lean4

/-- Subsequent Fibonacci numbers are coprime,
  see https://proofwiki.org/wiki/Consecutive_Fibonacci_Numbers_are_Coprime -/
theorem fib_coprime_fib_succ (n : ℕ) : Nat.Coprime (fib n) (fib (n + 1)) := by
  induction n with
  | zero => simp
  | succ n ih => simp only [fib_add_two, coprime_add_self_right, Coprime, ih.symm]

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