Theorem: DividedPowerAlgebra.dpScalarExtension_tmul (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
r : R
m : DividedPowerAlgebra A M
⊢ (dpScalarExtension A R M) (r ⊗ₜ[A] m) = r • (dpScalarExtension A R M) (1 ⊗ₜ[A] m)
Tactic:
simp only [dpScalarExtension, AlgHom.baseChange_tmul, one_smul]
State after:
no goals