fib_gcd — Mathlib

English

For all m,n, fib(gcd(m,n)) = gcd(fib(m), fib(n)).

Русский

Для всех m,n выполнено fib(gcd(m,n)) = gcd(fib(m), fib(n)).

LaTeX

$$fib(gcd(m,n)) = gcd(fib(m), fib(n))$$

Lean4

/-- `fib n` is a strong divisibility sequence,
  see https://proofwiki.org/wiki/GCD_of_Fibonacci_Numbers -/
theorem fib_gcd (m n : ℕ) : fib (gcd m n) = gcd (fib m) (fib n) := by
  induction m, n using Nat.gcd.induction with
  | H0 => simp
  | H1 m n _ h' =>
    rw [← gcd_rec m n] at h'
    conv_rhs => rw [← mod_add_div' n m]
    rwa [gcd_fib_add_mul_self m (n % m) (n / m), gcd_comm (fib m) _]

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