Theorem: DividedPowerAlgebra.liftAlgHom_apply_dp (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
n : ℕ
m : M
⊢ (lift hI φ hφ) (dp R n m) = hI.dpow n (φ m)
Tactic:
rw [lift, lift'AlgHom_apply_dp]
State after:
no goals