rTensor_apply_monomial_tmul — Mathlib

English

If e is a finsupp on σ, and s ∈ S, then rTensor applied to monomial e with coefficient s tensored with n yields if e = d then s ⊗ n else 0.

Русский

Если e — фиктивный мономиал и s ∈ S, то образ rTensor(monomial e s ⊗ n) по координате d равен s ⊗ n, когда e = d, иначе 0.

LaTeX

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

Lean4

theorem rTensor_apply_monomial_tmul (e : σ →₀ ℕ) (s : S) (n : N) (d : σ →₀ ℕ) :
    rTensor (monomial e s ⊗ₜ[R] n) d = if e = d then s ⊗ₜ[R] n else 0 := by
  simp only [rTensor_apply_tmul_apply, coeff_monomial, ite_tmul]

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