Theorem: MonoidAlgebra.algHom_apply_apply (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
x : MonoidAlgebra N α
a : α
⊢ ((algHom e) x) a = e (x a)
Tactic:
simp [algHom]
State after:
no goals