Theorem TensorProduct.exists_finite_submodule_left_of_setFinite

Modification history

2025-10-11 22:15
Mathlib/LinearAlgebra/TensorProduct/Finiteness.lean
chore(LinearAlgebra/TensorProduct/Finiteness): rename `_of_finite` lemmas to `_of_setFinite` (#30435) …
Added TensorProduct.exists_finite_submodule_left_of_setFiniteView on Github →