periodic_gcd

Mathlib.Data.Nat.Periodic

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

English

For any a, the function n ↦ gcd(a, n) is periodic with period a; i.e., gcd(a, n+a) = gcd(a, n) for all n.

Русский

Для любого a функция n ↦ gcd(a, n) периодична с периодом a; т.е. gcd(a, n+a) = gcd(a, n) для всех n.

LaTeX

$$$ \forall n, \gcd(a, n+a) = \gcd(a, n) $$$

Lean4

theorem periodic_gcd (a : ℕ) : Periodic (gcd a) a := by simp only [forall_const, gcd_add_self_right, Periodic]

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

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

Разделы

Аффилиация

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