no goals
α : Type u_2
β : Type ?u.645727
γ : Type ?u.645730
ι : Type ?u.645733
M : Type ?u.645736
M' : Type ?u.645739
N : Type ?u.645742
P : Type ?u.645745
G : Type ?u.645748
H : Type ?u.645751
R : Type u_1
S : Type ?u.645757
inst✝ : Semiring R
a : α
b : R
⊢ b • single a 1 = single a b
rw [smul_single, smul_eq_mul, mul_one]