sum_tmul_basis_left_eq_zero — Mathlib

English

If a left-basis sum vanishes, then all coefficients are zero.

Русский

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

LaTeX

$$(b : ι →₀ N) (h : (b.sum (fun i n ⇒ ℬ i ⊗ₜ R n)) = 0) : b = 0$$

Lean4

theorem sum_tmul_basis_left_eq_zero (b : ι →₀ N) (h : (b.sum fun i n ↦ ℬ i ⊗ₜ[R] n) = 0) : b = 0 :=
  have := Classical.decEq ι
  (TensorProduct.equivFinsuppOfBasisLeft ℬ).symm.injective (a₂ := 0) <| by simpa

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