Theorem TensorProduct.exists_finite_submodule_left_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_left_of_finite'View 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_left_of_finite'View on Github →