no goals
α : Type ?u.278192
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Ring R
a : R
n : ℤ
⊢ n • a = a * ↑n
rw [zsmul_eq_mul, (n.cast_commute a).eq]