@[simp]

theorem AddMonoidAlgebra.single_ne_zero {k : Type u_1} [Semiring k] {G : Type u_2} {a : G} {b : k} : single a b ≠ 0 ↔ b ≠ 0