Theorem: Polynomial.scalarRTensor_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
pn : R[X] ⊗[R] N
d : ℕ
⊢ ((scalarRTensor R N) pn) d = (TensorProduct.lid R N) ((LinearMap.rTensor N (lcoeff R d)) pn)
Tactic:
rw [← LinearEquiv.symm_apply_eq, lid_symm_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
pn : R[X] ⊗[R] N
d : ℕ
⊢ 1 ⊗ₜ[R] ((scalarRTensor R N) pn) d = (LinearMap.rTensor N (lcoeff R d)) pn

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
pn : R[X] ⊗[R] N
d : ℕ
⊢ 1 ⊗ₜ[R] ((scalarRTensor R N) pn) d = (LinearMap.rTensor N (lcoeff R d)) pn
Tactic:
induction pn using TensorProduct.induction_on with
| zero => simp
| tmul p n => simp [scalarRTensor_apply_tmul_apply, TensorProduct.smul_tmul']
| add x y hx hy => simp [tmul_add, hx, hy]
State after:
no goals

State before:
case zero
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
d : ℕ
⊢ 1 ⊗ₜ[R] ((scalarRTensor R N) 0) d = (LinearMap.rTensor N (lcoeff R d)) 0
Tactic:
simp
State after:
no goals

State before:
case tmul
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
d : ℕ
p : R[X]
n : N
⊢ 1 ⊗ₜ[R] ((scalarRTensor R N) (p ⊗ₜ[R] n)) d = (LinearMap.rTensor N (lcoeff R d)) (p ⊗ₜ[R] n)
Tactic:
simp [scalarRTensor_apply_tmul_apply, TensorProduct.smul_tmul']
State after:
no goals

State before:
case add
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
d : ℕ
x y : R[X] ⊗[R] N
hx : 1 ⊗ₜ[R] ((scalarRTensor R N) x) d = (LinearMap.rTensor N (lcoeff R d)) x
hy : 1 ⊗ₜ[R] ((scalarRTensor R N) y) d = (LinearMap.rTensor N (lcoeff R d)) y
⊢ 1 ⊗ₜ[R] ((scalarRTensor R N) (x + y)) d = (LinearMap.rTensor N (lcoeff R d)) (x + y)
Tactic:
simp [tmul_add, hx, hy]
State after:
no goals