no goals
α : Type u_1
β : Type u_2
γ : Type ?u.156251
f g : α → β
c c₁ c₂ x : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
⊢ Antiperiodic f (-c)
simpa only [sub_eq_add_neg, Antiperiodic] using h.sub_eq