R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.1304029
inst✝¹³ : Monoid R'
R'' : Type ?u.1304035
inst✝¹² : Semiring R''
M : Type u_3
N : Type u_2
P : Type ?u.1304047
Q : Type ?u.1304050
S : Type ?u.1304053
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : AddCommMonoid S
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module R S
inst✝¹ : DistribMulAction R' M
inst✝ : Module R'' M
g : P →ₗ[R] Q
f✝ : N →ₗ[R] P
f : N →ₗ[R] N
n : ℕ
h : map id f ^ n = map (id ^ n) (f ^ n)
⊢ lTensor M f ^ n = lTensor M (f ^ n)
R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.1304029
inst✝¹³ : Monoid R'
R'' : Type ?u.1304035
inst✝¹² : Semiring R''
M : Type u_3
N : Type u_2
P : Type ?u.1304047
Q : Type ?u.1304050
S : Type ?u.1304053
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : AddCommMonoid S
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module R S
inst✝¹ : DistribMulAction R' M
inst✝ : Module R'' M
g : P →ₗ[R] Q
f✝ : N →ₗ[R] P
f : N →ₗ[R] N
n : ℕ
⊢ lTensor M f ^ n = lTensor M (f ^ n)
have h := TensorProduct.map_pow (id : M →ₗ[R] M) f n
no goals
R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.1304029
inst✝¹³ : Monoid R'
R'' : Type ?u.1304035
inst✝¹² : Semiring R''
M : Type u_3
N : Type u_2
P : Type ?u.1304047
Q : Type ?u.1304050
S : Type ?u.1304053
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : AddCommMonoid S
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module R S
inst✝¹ : DistribMulAction R' M
inst✝ : Module R'' M
g : P →ₗ[R] Q
f✝ : N →ₗ[R] P
f : N →ₗ[R] N
n : ℕ
h : map id f ^ n = map (id ^ n) (f ^ n)
⊢ lTensor M f ^ n = lTensor M (f ^ n)
rwa [id_pow] at h