smul — Mathlib

English

If f is c-periodic, then for any scalar a, the function x ↦ a · f(x) is c-periodic.

Русский

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

LaTeX

$$$\\forall f:\\alpha→β, \\forall c:\\alpha, Periodic(f,c) ⇒ \\forall a:\\gamma, Periodic(a·f,c)$$$

Lean4

@[to_additive]
protected theorem smul [Add α] [SMul γ β] (h : Periodic f c) (a : γ) : Periodic (a • f) c := by simp_all

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