const_inv_smul₀ — Mathlib

English

If f is periodic with period c, then the function x ↦ f(a·x) is periodic with the same pattern scaled by a.

Русский

Если f периодична с периодом c, то x ↦ f(a·x) периодична с тем же рисунком, масштабированным на a.

LaTeX

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

Lean4

theorem const_inv_smul₀ [AddCommMonoid α] [DivisionSemiring γ] [Module γ α] (h : Periodic f c) (a : γ) :
    Periodic (fun x => f (a⁻¹ • x)) (a • c) := by simpa only [inv_inv] using h.const_smul₀ a⁻¹

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