@[simp]

theorem MonoidAlgebra.domCongr_comp_lsingle {R : Type u_1} {A : Type u_2} {G : Type u_3} {H : Type u_4} [CommSemiring R] [Monoid G] [Monoid H] [Semiring A] [Algebra R A] (e : G ≃* H) (g : G) : (domCongr R A e).toLinearMap ∘ₗ lsingle g = lsingle (e g)

@[simp]

theorem AddMonoidAlgebra.domCongr_comp_lsingle {R : Type u_1} {A : Type u_2} {G : Type u_3} {H : Type u_4} [CommSemiring R] [AddMonoid G] [AddMonoid H] [Semiring A] [Algebra R A] (e : G ≃+ H) (g : G) : (domCongr R A e).toLinearMap ∘ₗ lsingle g = lsingle (e g)