finsuppLeft_apply_tmul_apply — Mathlib

English

The i-th coordinate of the image equals p_i ⊗ n under the finsuppLeft isomorphism.

Русский

i-я координата образа равна p_i ⊗ n под изоморфизмом finsuppLeft.

LaTeX

$$$finsuppLeft R M N ι (p \\otimes_R n) i = p_i \\otimes_R n$$$

Lean4

@[simp]
theorem finsuppLeft_apply_tmul_apply (p : ι →₀ M) (n : N) (i : ι) : finsuppLeft R M N ι (p ⊗ₜ[R] n) i = p i ⊗ₜ[R] n :=
  by
  rw [finsuppLeft_apply_tmul, Finsupp.sum_apply, Finsupp.sum_eq_single i (fun _ _ ↦ Finsupp.single_eq_of_ne') (by simp),
    Finsupp.single_eq_same]

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