no goals
α : Type u_1
β : Type u_3
γ : Type u_2
f g : α → β
c c₁ c₂ x : α
inst✝² : AddCommMonoid α
inst✝¹ : DivisionSemiring γ
inst✝ : Module γ α
h : Periodic f c
a : γ
⊢ Periodic (fun x => f (a⁻¹ • x)) (a • c)
simpa only [inv_inv] using h.const_smul₀ a⁻¹