rTensor_apply — Mathlib

English

For t ∈ MvPolynomial σ S ⊗_R N and each d, the d-coordinate of rTensor t equals the application of lcoeff_S d to t via restriction of scalars and the rTensor construction.

Русский

Для произвольного t из MvPolynomial σ S ⊗_R N координата d равна применению lcoeff_S d к t с учётом ограничения скаляров и построения rTensor.

LaTeX

$$$rTensor\\; t\\; d = ((lcoeff\\; S\\; d).restrictScalars\\; R).rTensor\\; N\\; t$$$

Lean4

theorem rTensor_apply (t : MvPolynomial σ S ⊗[R] N) (d : σ →₀ ℕ) :
    rTensor t d = ((lcoeff S d).restrictScalars R).rTensor N t :=
  TensorProduct.finsuppLeft_apply t d

Похожие утверждения