Theorem: DividedPowerAlgebra.dp_smul (DividedPowers/DPAlgebra/Init.lean)

State before:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
n : ℕ
m : M
⊢ dp R n (r • m) = r ^ n • dp R n m
Tactic:
rw [dp_def, dp_def, ← map_smul]
State after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
n : ℕ
m : M
⊢ (mkAlgHom R (Rel R M)) (X (n, r • m)) = (mkAlgHom R (Rel R M)) (r ^ n • X (n, m))

State before:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
n : ℕ
m : M
⊢ (mkAlgHom R (Rel R M)) (X (n, r • m)) = (mkAlgHom R (Rel R M)) (r ^ n • X (n, m))
Tactic:
exact mkAlgHom_rel R Rel.smul
State after:
no goals