Commit 2025-10-11 22:15 698d3067
View on Github →chore(LinearAlgebra/TensorProduct/Finiteness): rename _of_finite lemmas to _of_setFinite (#30435)
TensorProduct.exists_finite_submodule_of_finite and its variants are confusing since the finite in the name refers to different things, so we change it to _of_setFinite.