scalarRTensor_symm_apply_single — Mathlib

English

For e ∈ σ →₀ ℕ, s ∈ S, n ∈ N, d ∈ σ →₀ ℕ, the coefficient at d of rTensorAlgHom(monomial e s ⊗ n) equals if e = d then s ⊗ n else 0.

Русский

Для e, s, n, d: coeff d (rTensorAlgHom(monomial e s ⊗ n)) = if e = d then s ⊗ n else 0.

LaTeX

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

Lean4

theorem scalarRTensor_symm_apply_single (d : σ →₀ ℕ) (n : N) :
    scalarRTensor.symm (Finsupp.single d n) = (monomial d 1) ⊗ₜ[R] n :=
  TensorProduct.finsuppScalarLeft_symm_apply_single d n

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