finsuppLeft_apply_tmul — Mathlib

English

The equivalence applied to a pure tensor p ⊗ n yields the corresponding simple tensors coordinated by p.

Русский

Применение эквивалентности к чистому тензору p ⊗ n возвращает соответствующие простые тензоры, координаты которыми задаёт p.

LaTeX

$$$finsuppLeft R M N ι (p \\otimes_R n) = p.sum (i \\mapsto Finsupp.single i (m_i \\otimes_R n))$$$

Lean4

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

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