Theorem: DividedPowerAlgebra.liftAlgHom_apply_dp (unused_files/Init_copy.lean)

State before:
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing 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