nat_mul — Mathlib

English

If f is c-periodic, then f is (n·c)-periodic for natural n.

Русский

Если f периодична по c, то она периодична по n·c для любого натурального n.

LaTeX

$$$\\forall f:\\alpha→β, \\forall c:\\alpha, Periodic(f,c) ⇒ \\forall n:\\mathbb{N}, Periodic(f(n\\cdot c),) $$$

Lean4

theorem nat_mul [NonAssocSemiring α] (h : Periodic f c) (n : ℕ) : Periodic f (n * c) := by
  simpa only [nsmul_eq_mul] using h.nsmul n

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