const_inv_smul — Mathlib

English

If f is periodic with periods c1 and c2, then f is periodic with period c1 + c2.

Русский

Если функция периодична с периодами c1 и c2, то она периодична и с периодом c1 + c2.

LaTeX

$$$\\forall f:\\alpha→β, \\forall c_1,c_2:\\alpha, Periodic(f,c_1) ∧ Periodic(f,c_2) ⇒ Periodic(f, c_1+c_2)$$$

Lean4

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

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