no goals
k : Type u₁
G : Type u₂
R : Type ?u.1010908
A : Type u_1
inst✝³ : CommSemiring k
inst✝² : Semiring A
inst✝¹ : Algebra k A
inst✝ : Monoid G
a : G
b : k
⊢ single a (↑(algebraMap k A) b) = ↑(algebraMap k (MonoidAlgebra A G)) b * ↑(of A G) a
simp