Finiteness of tensor product

Stream: Is there code for X?

[Antoine Labelle]

Do we have the fact that if M and N are finite R modules, so is M ⊗ N?

[Eric Wieser]

docs#finite_dimensional_tensor_product

[Eric Wieser]

Probably the existing proof can be generalized to commutative rings

[Antoine Labelle]

Yes I'd want that for arbitrary commutative rings

[Antoine Labelle]

The proof doesn't immediatly generalize since in general we don't have bases, but it shouldn't be too hard.

[Riccardo Brasca]

I would prove that a module is finite iff it is the image of a surjective hom from a finite and free module (this shuld be very easy, but I think it is missing), and then use the universal property of tensor product of the two free modules to produce the surjection you need.

[Junyan Xu]

#13705