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