div_const — Mathlib

English

If f is periodic with period c, then f(x/a) is periodic with period c·a.

Русский

Если f периодична с периодом c, то f(x/a) периодична с периодом c·a.

LaTeX

$$$\text{Periodic}(f,c)\Rightarrow \forall a, \text{Periodic}(\lambda x. f(x\,/\ a), c\cdot a)$$$

Lean4

theorem div_const [DivisionSemiring α] (h : Periodic f c) (a : α) : Periodic (fun x => f (x / a)) (c * a) := by
  simpa only [div_eq_mul_inv] using h.mul_const_inv a

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