no goals
α : Type u_1
β : Type u_2
γ : Type ?u.162678
f g : α → β
c c₁ c₂ x : α
inst✝¹ : Ring α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
hi : f 0 = 0
n : ℕ
⊢ f (↑↑n * c) = 0
rw [Int.cast_ofNat, h.nat_mul_eq_of_eq_zero hi n]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.162678
f g : α → β
c c₁ c₂ x : α
inst✝¹ : Ring α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
hi : f 0 = 0
n : ℕ
⊢ f (↑(Int.negSucc n) * c) = 0
rw [Int.cast_negSucc, neg_mul, ← mul_neg, h.neg.nat_mul_eq_of_eq_zero hi]