Theorem: Polynomial.scalarRTensor_apply_tmul_apply (DividedPowers/ForMathlib/RingTheory/TensorProduct/Polynomial.lean)

State before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ ((scalarRTensor R N) (p ⊗ₜ[R] n)) i = p.coeff i • n
Tactic:
simp only [scalarRTensor, LinearEquiv.trans_apply]
State after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ ((finsuppScalarLeft R N ℕ) ((LinearEquiv.rTensor N (toFinsuppLinearEquiv R)) (p ⊗ₜ[R] n))) i = p.coeff i • n

State before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ ((finsuppScalarLeft R N ℕ) ((LinearEquiv.rTensor N (toFinsuppLinearEquiv R)) (p ⊗ₜ[R] n))) i = p.coeff i • n
Tactic:
simp only [LinearEquiv.rTensor, congr_tmul, refl_apply]
State after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ ((finsuppScalarLeft R N ℕ) ((toFinsuppLinearEquiv R) p ⊗ₜ[R] n)) i = p.coeff i • n

State before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ ((finsuppScalarLeft R N ℕ) ((toFinsuppLinearEquiv R) p ⊗ₜ[R] n)) i = p.coeff i • n
Tactic:
rw [finsuppScalarLeft_apply_tmul_apply _ n i]
State after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ ((toFinsuppLinearEquiv R) p) i • n = p.coeff i • n

State before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ ((toFinsuppLinearEquiv R) p) i • n = p.coeff i • n
Tactic:
rfl
State after:
no goals