Theorem: MonoidAlgebra.algHom_apply_single (DividedPowers/ForMathlib/RingTheory/TensorProduct/MonoidAlgebra.lean)

State before:
α : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁶ : DecidableEq α
inst✝⁵ : Semiring N
inst✝⁴ : Semiring P
inst✝³ : Monoid α
inst✝² : CommSemiring R
inst✝¹ : Algebra R N
inst✝ : Algebra R P
e : N →ₐ[R] P
a : α
n : N
⊢ (algHom e) (single a n) = single a (e n)
Tactic:
simp [algHom]
State after:
no goals