gcd — Mathlib

English

If x is periodic with period n, then f^{m mod n} (x) = f^{m}(x) for all m.

Русский

Если x имеет период n, то f^{m mod n}(x) = f^{m}(x) для всех m.

LaTeX

$$$IsPeriodicPt f n x \to \forall m, f^{m \% n}(x) = f^{m}(x)$$$

Lean4

protected theorem gcd (hm : IsPeriodicPt f m x) (hn : IsPeriodicPt f n x) : IsPeriodicPt f (m.gcd n) x :=
  by
  revert hm hn
  refine Nat.gcd.induction m n (fun n _ hn => ?_) fun m n _ ih hm hn => ?_
  · rwa [Nat.gcd_zero_left]
  · rw [Nat.gcd_rec]
    exact ih (hn.mod hm) hm

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