Theorem TensorProduct.exists_finite_submodule_of_finite

Modification history

2025-10-11 22:15
Mathlib/LinearAlgebra/TensorProduct/Finiteness.lean
chore(LinearAlgebra/TensorProduct/Finiteness): rename `_of_finite` lemmas to `_of_setFinite` (#30435) …
Deleted TensorProduct.exists_finite_submodule_of_finiteView on Github →
2024-04-14 05:44
Mathlib/LinearAlgebra/TensorProduct/Finiteness.lean
feat(LinearAlgebra/TensorProduct/Finiteness): add some finiteness results of tensor product (#11859) …
Added TensorProduct.exists_finite_submodule_of_finiteView on Github →