periodic_coprime — Mathlib

English

For any a, the predicate n ↦ Coprime(a, n) is periodic with period a; i.e., Coprime(a, n+a) ↔ Coprime(a, n).

Русский

Для любого a предикат n ↦ Coprime(a, n) периодичен с периодом a; то есть Coprime(a, n+a) ↔ Coprime(a, n).

LaTeX

$$$ \forall n, \operatorname{Coprime}(a, n+a) \iff \operatorname{Coprime}(a, n) $$$

Lean4

theorem periodic_coprime (a : ℕ) : Periodic (Coprime a) a := by
  simp only [coprime_add_self_right, forall_const, Periodic]

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