const_smul — Mathlib

English

If f is c-periodic, then f(x − c) = f(x) for all x.

Русский

Если f периодична с периодом c, то для любого x выполняется f(x − c) = f(x).

LaTeX

$$$\\forall f:\\alpha→β, \\forall c:\\alpha, Periodic(f,c) ⇒ \\forall x:\\alpha, f(x-c) = f(x)$$$

Lean4

protected theorem const_smul [AddMonoid α] [Group γ] [DistribMulAction γ α] (h : Periodic f c) (a : γ) :
    Periodic (fun x => f (a • x)) (a⁻¹ • c) := fun x => by simpa only [smul_add, smul_inv_smul] using h (a • x)

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