Commit 2024-04-14 05:44 79d6c97c

View on Github →

feat(LinearAlgebra/TensorProduct/Finiteness): add some finiteness results of tensor product (#11859)

  • TensorProduct.exists_multiset, TensorProduct.exists_finsupp_left, TensorProduct.exists_finsupp_right, TensorProduct.exists_finset: any element of M ⊗[R] N can be written as a finite sum of pure tensors. See also TensorProduct.span_tmul_eq_top.
  • TensorProduct.exists_finite_submodule_left_of_finite, TensorProduct.exists_finite_submodule_right_of_finite, TensorProduct.exists_finite_submodule_of_finite and 3 more: any finite subset of M ⊗[R] N is contained in M' ⊗[R] N' for some finitely generated submodules M' and N' of M and N, respectively. Each of these 3 functions has 2 variants.

Estimated changes