Theorem: DividedPowerAlgebra.LinearMap.liftAlgHom_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
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
n : ℕ
a : M
⊢ (lift R S f) (dp R n a) = dp S n (f a)
Tactic:
rw [LinearMap.lift, lift'AlgHom_apply_dp]
State after:
no goals