rTensor_apply_X_tmul — Mathlib

English

For a basis symbol X_s, the image rTensor(X_s ⊗ n) at d is 1 ⊗ n when d equals the singleton at s, and 0 otherwise.

Русский

Для X_s образ rTensor(X_s ⊗ n) на координате d равен 1 ⊗ n, когда d = single(s,1); иначе 0.

LaTeX

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

Lean4

theorem rTensor_apply_X_tmul (s : σ) (n : N) (d : σ →₀ ℕ) :
    rTensor (X s ⊗ₜ[R] n) d = if Finsupp.single s 1 = d then (1 : S) ⊗ₜ[R] n else 0 := by
  rw [rTensor_apply_tmul_apply, coeff_X', ite_tmul]

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