no goals
α : Type ?u.325888
R✝ : Type ?u.325891
k : Type ?u.325894
S : Type ?u.325897
M : Type ?u.325900
M₂ : Type ?u.325903
M₃ : Type ?u.325906
ι : Type ?u.325909
R : Type u_1
inst✝ : Ring R
m : ℤ
⊢ m • 1 = ↑m
rw [zsmul_eq_mul, mul_one]