English
Again, the coefficient at d of rTensorAlgHom(monomial e s ⊗ n) equals if e = d then s ⊗ n else 0.
Русский
Коэффициент coeff d (rTensorAlgHom(monomial e s ⊗ n)) равен, если e = d, то s ⊗ n, иначе 0.
LaTeX
$$$coeff d (rTensorAlgHom (\\mathrm{monomial}\\, e\\, s ⊗ n)) = \\begin{cases} s \\otimes n, & e = d, \\\\ 0, & \\text{иначе}. \\end{cases}$$$
Lean4
theorem rTensorAlgHom_toLinearMap :
(rTensorAlgHom : MvPolynomial σ S ⊗[R] N →ₐ[S] MvPolynomial σ (S ⊗[R] N)).toLinearMap = rTensor.toLinearMap :=
by
ext d n e
dsimp only [AlgebraTensorModule.curry_apply, TensorProduct.curry_apply, LinearMap.coe_restrictScalars,
AlgHom.toLinearMap_apply]
simp only [coe_comp, Function.comp_apply, AlgebraTensorModule.curry_apply, curry_apply, LinearMap.coe_restrictScalars,
AlgHom.toLinearMap_apply]
rw [coeff_rTensorAlgHom_tmul]
simp only [coeff]
exact (finsuppLeft_apply_tmul_apply _ _ _).symm
