Theorem: DividedPowerAlgebra.LinearMap.liftAlgHom_apply (DividedPowers/DPAlgebra/Init.lean)

State before:
R : Type u_1
M : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
S : Type u_3
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
N : Type u_4
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
p : MvPolynomial (ℕ × M) R
⊢ (lift R S f) (mk p) = (aeval fun nm => dp S nm.1 (f nm.2)) p
Tactic:
rw [LinearMap.lift, lift'AlgHom_apply]
State after:
no goals