Theorem: DividedPowerAlgebra.dpScalarExtension_apply_one_dp (DividedPowers/DPAlgebra/BaseChange.lean)

State before:
A : Type u_1
inst✝⁴ : CommSemiring A
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : Algebra A R
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
n : ℕ
m : M
⊢ (dpScalarExtension A R M) (1 ⊗ₜ[A] dp A n m) = dp R n (1 ⊗ₜ[A] m)
Tactic:
rw [← one_pow n, dpScalarExtension_apply_dp, one_pow]
State after:
no goals