finsuppRight_apply_tmul — Mathlib

English

For m ∈ M and p ∈ ι →₀ N, the image of m ⊗ p under finsuppRight, evaluated at i, is the simple tensor m ⊗ p(i).

Русский

Для m ∈ M и p ∈ ι →₀ N, значение finsuppRight при m ⊗ p в точке i равно m ⊗ p(i).

LaTeX

$$$ finsuppRight R M N ι (m \\otimes p) (i) = m \\otimes (p(i)) $$$

Lean4

theorem finsuppRight_apply_tmul (m : M) (p : ι →₀ N) :
    finsuppRight R M N ι (m ⊗ₜ[R] p) = p.sum fun i n ↦ Finsupp.single i (m ⊗ₜ[R] n) := by
  induction p using Finsupp.induction_linear with
  | zero => simp
  | add f g hf hg => simp [tmul_add, map_add, hf, hg, Finsupp.sum_add_index]
  | single => simp [finsuppRight]

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