no goals
α : Type u_1
β : Type u_2
γ : Type ?u.70814
f g : α → β
c c₁ c₂ x : α
inst✝ : DivisionSemiring α
h : Periodic f c
a : α
⊢ Periodic (fun x => f (x * a)) (c / a)
simpa only [div_eq_mul_inv] using h.mul_const a