case ofNat
α : Type u_1
β : Type u_2
γ : Type ?u.104199
f g : α → β
c c₁ c₂ x : α
inst✝ : AddGroup α
h : Periodic f c
n : ℕ
⊢ Periodic f (Int.ofNat n • c)

case negSucc
α : Type u_1
β : Type u_2
γ : Type ?u.104199
f g : α → β
c c₁ c₂ x : α
inst✝ : AddGroup α
h : Periodic f c
n : ℕ
⊢ Periodic f (Int.negSucc n • c)
α : Type u_1
β : Type u_2
γ : Type ?u.104199
f g : α → β
c c₁ c₂ x : α
inst✝ : AddGroup α
h : Periodic f c
n : ℤ
⊢ Periodic f (n • c)
cases' n with n n
no goals
case ofNat
α : Type u_1
β : Type u_2
γ : Type ?u.104199
f g : α → β
c c₁ c₂ x : α
inst✝ : AddGroup α
h : Periodic f c
n : ℕ
⊢ Periodic f (Int.ofNat n • c)
simpa only [Int.ofNat_eq_coe, coe_nat_zsmul] using h.nsmul n
no goals
case negSucc
α : Type u_1
β : Type u_2
γ : Type ?u.104199
f g : α → β
c c₁ c₂ x : α
inst✝ : AddGroup α
h : Periodic f c
n : ℕ
⊢ Periodic f (Int.negSucc n • c)
simpa only [negSucc_zsmul] using (h.nsmul (n + 1)).neg