scalarRTensor_apply_monomial_tmul

English

For e ∈ σ →₀ ℕ and r ∈ R, the scalarRTensor of monomial e r tensored with n has coordinates d equal to r · n when e = d and 0 otherwise.

Русский

Для e мономиала и коэффициента r, образ scalarRTensor(monomial e r ⊗ n) имеет координаты d, равные r · n, если e = d, иначе 0.

LaTeX

$$$\\text{scalarRTensor}(\\mathrm{monomial}\\, e\\, r \\otimes n)\\; d = \\begin{cases} r \\cdot n, & e = d, \\\\ 0, & \\text{иначе}. \\end{cases}$$$

Lean4

theorem scalarRTensor_apply_monomial_tmul (e : σ →₀ ℕ) (r : R) (n : N) (d : σ →₀ ℕ) :
    scalarRTensor (monomial e r ⊗ₜ[R] n) d = if e = d then r • n else 0 := by
  rw [scalarRTensor_apply_tmul_apply, coeff_monomial, ite_smul, zero_smul]

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