Theorem: DividedPowerAlgebra.LinearMap.dp_smul (unused_files/Init_copy.lean)

State before:
R : Type u_4
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
S : Type u_1
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
N : Type u_2
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
inst✝¹ : Algebra R (DividedPowerAlgebra S N)
inst✝ : IsScalarTower R S (DividedPowerAlgebra 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_4
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
S : Type u_1
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
N : Type u_2
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
inst✝¹ : Algebra R (DividedPowerAlgebra S N)
inst✝ : IsScalarTower R S (DividedPowerAlgebra 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_4
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
S : Type u_1
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
N : Type u_2
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
inst✝¹ : Algebra R (DividedPowerAlgebra S N)
inst✝ : IsScalarTower R S (DividedPowerAlgebra 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_4
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
S : Type u_1
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
N : Type u_2
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
inst✝¹ : Algebra R (DividedPowerAlgebra S N)
inst✝ : IsScalarTower R S (DividedPowerAlgebra 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_4
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
S : Type u_1
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
N : Type u_2
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
inst✝¹ : Algebra R (DividedPowerAlgebra S N)
inst✝ : IsScalarTower R S (DividedPowerAlgebra 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, ← algebra_compatible_smul]
State after:
R : Type u_4
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
S : Type u_1
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
N : Type u_2
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
inst✝¹ : Algebra R (DividedPowerAlgebra S N)
inst✝ : IsScalarTower R S (DividedPowerAlgebra 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)