gcd_fib_add_mul_self

Mathlib.Data.Nat.Fib.Basic

URI: https://scilib.ai/kg/mathlib#Nat.gcd_fib_add_mul_self

← MathLib Explorer

English

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

Русский

Для всех m,n,k верно gcd(F_m, F_{n + k m}) = gcd(F_m, F_n).

LaTeX

$$gcd(fib(m), fib(n + k*m)) = gcd(fib(m), fib(n))$$

Lean4

theorem gcd_fib_add_mul_self (m n : ℕ) : ∀ k, gcd (fib m) (fib (n + k * m)) = gcd (fib m) (fib n)
  | 0 => by simp
  | k + 1 => by rw [← gcd_fib_add_mul_self m n k, add_mul, ← add_assoc, one_mul, gcd_fib_add_self _ _]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru