no goals
α : Type u_1
β : Type u_2
γ : Type ?u.160104
f g : α → β
c c₁ c₂ x : α
inst✝¹ : Semiring α
inst✝ : NegZeroClass β
h : Antiperiodic f c
hi : f 0 = 0
⊢ f (↑0 * c) = 0
rwa [Nat.cast_zero, zero_mul]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.160104
f g : α → β
c c₁ c₂ x : α
inst✝¹ : Semiring α
inst✝ : NegZeroClass β
h : Antiperiodic f c
hi : f 0 = 0
n : ℕ
⊢ f (↑(n + 1) * c) = 0
simp [add_mul, h _, Antiperiodic.nat_mul_eq_of_eq_zero h hi n]