no goals
G : Type ?u.29474
inst✝³ : Group G
A : Type ?u.29480
inst✝² : AddGroup A
N : Type ?u.29486
inst✝¹ : Group N
R : Type u_1
inst✝ : Ring R
r : R
k : ℤ
⊢ ↑k * r ∈ zmultiples r
simpa only [← zsmul_eq_mul] using zsmul_mem_zmultiples r k