Theorem: DividedPowerAlgebra.LinearMap.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
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
r : R
n : ℕ
a : M
⊢ dp S n (f (r • a)) = r ^ n • dp S n (f a)
Tactic:
rw [f.map_smul, algebra_compatible_smul S r (f a)]
State after:
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
r : R
n : ℕ
a : M
⊢ dp S n ((algebraMap R S) r • f a) = r ^ n • dp S n (f a)

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
r : R
n : ℕ
a : M
⊢ dp S n ((algebraMap R S) r • f a) = r ^ n • dp S n (f a)
Tactic:
rw [DividedPowerAlgebra.dp_smul S ((algebraMap R S) r) n (f a)]
State after:
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
r : R
n : ℕ
a : M
⊢ (algebraMap R S) r ^ n • dp S n (f a) = r ^ n • dp S n (f a)

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
r : R
n : ℕ
a : M
⊢ (algebraMap R S) r ^ n • dp S n (f a) = r ^ n • dp S n (f a)
Tactic:
rw [← map_pow, algebraMap_smul]
State after:
no goals