int_mul — Mathlib

English

Let f: α → β be periodic with period c ∈ α. Then for every integer n, f has period n·c; equivalently, f(x + n·c) = f(x) for all x ∈ α and all n ∈ ℤ.

Русский

Пусть f: α → β периодична с периодом c ∈ α. Тогда для каждого целого числа n функция f имеет период n·c; то есть для всех x ∈ α и всех n ∈ ℤ выполняется f(x + n·c) = f(x).

LaTeX

$$$\forall f:\alpha \to \beta, \forall c\in \alpha,\big(\forall x:\alpha,\ f(x+c)=f(x)\big) \Rightarrow \forall n\in \mathbb{Z},\forall x:\alpha,\ f(x+n c)=f(x).$$$

Lean4

protected theorem int_mul [NonAssocRing α] (h : Periodic f c) (n : ℤ) : Periodic f (n * c) := by
  simpa only [zsmul_eq_mul] using h.zsmul n

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