sum_tmul_basis_left_injective — Mathlib

English

The left-sum map using the left basis is injective.

Русский

Левый суммирующий оператор по базису инъективен.

LaTeX

$$Function.Injective (Finsupp.lsum R fun i ⇢ (TensorProduct.mk R M N) (ℬ i))$$

Lean4

theorem sum_tmul_basis_left_injective : Function.Injective (Finsupp.lsum R fun i ↦ (TensorProduct.mk R M N) (ℬ i)) :=
  have := Classical.decEq ι
  (equivFinsuppOfBasisLeft_symm (N := N) ℬ).symm ▸ (TensorProduct.equivFinsuppOfBasisLeft ℬ).symm.injective

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