basis.tensor_product

Stream: maths

[Jakob von Raumer]

What does basis.tensor_product do in linear_algebra.finsupp_vector_space? It's neither about modules which are necessarily vector spaces, nor about finiteness...

[Anne Baanen]

IIRC, the definitions in finsupp_vector_space.lean are finsupp-specific results that can't go in finsupp.lean because they depend on basis.lean, which depends on finsupp.lean.

[Anne Baanen]

In this case, looks like docs#finsupp.basis.tensor_product depends on docs#finsupp.basis_single_one, which is a basis for finsupp.

[Jakob von Raumer]

But basis.tensor_product itself isn't about finsupp at all, so why not put it in linear_algebra.tensor_product?

[Anne Baanen]

I don't know, and I think moving the definition should be a good idea, if the imports allow it. Looks like #3147 introduced basis.tensor_product, and there was no discussion on where to put it.

[Jakob von Raumer]

In a similar vein, finite_dimensional is lacking some instances, for products and, derived from that, for tensor products, right? Or am I just missing them?

[Anne Baanen]

I can't find them, no :/

[Anne Baanen]

I would like a big cleanup of some of those files in linear_algebra anyway, since I'm always having a lot of trouble finding things.

[Jakob von Raumer]

Might also be good to rename basis.ext, since it's not extensionality of bases but of linear maps..