Theorem: MvPolynomial.scalarRTensor_apply (DividedPowers/PolynomialMap/Coeff.lean)

State before:
R : Type u
inst✝⁷ : CommRing R
M : Type uM
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type uN
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
ι : Type uι
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
σ : Type u_1
inst✝ : DecidableEq σ
sn : MvPolynomial σ R ⊗[R] N
k : σ →₀ ℕ
⊢ (scalarRTensor sn) k = (TensorProduct.lid R N) ((LinearMap.rTensor N (lcoeff R k)) sn)
Tactic:
rw [← LinearEquiv.symm_apply_eq, TensorProduct.lid_symm_apply, rTensor_lcoeff]
State after:
no goals