Theorem: DividedPowerAlgebra.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
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
p : MvPolynomial (ℕ × M) R
⊢ (lift hI φ hφ) (mk p) = (aeval fun nm => hI.dpow nm.1 (φ nm.2)) p
Tactic:
rw [lift, lift'AlgHom_apply]
State after:
no goals