sum_tmul_basis_right_injective — Mathlib

English

If the right-tensor sum of basis elements with coefficients vanishes, then all coefficients are zero.

Русский

Если сумма коэффициентов по правому базису нулевая, то все коэффициенты равны нулю.

LaTeX

$$(b : κ →₀ M) \to (b.sum (fun i m ⇒ m ⊗ₜ 𝒞 i) = 0) → b = 0$$

Lean4

theorem sum_tmul_basis_right_injective :
    Function.Injective (Finsupp.lsum R fun i ↦ (TensorProduct.mk R M N).flip (𝒞 i)) :=
  have := Classical.decEq κ
  (equivFinsuppOfBasisRight_symm (M := M) 𝒞).symm ▸ (TensorProduct.equivFinsuppOfBasisRight 𝒞).symm.injective

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