Tensor linearly independent families

Stream: toric

[Paul Lezeau]

Yaël Dillies said:

• no one yet: Prove that the tensor product of two linearly independent families of vectors is linearly independent. cf. https://github.com/YaelDillies/Toric/blob/220af023b703a3bb77463a04f35c50f31c8c44e1/Toric/Mathlib/LinearAlgebra/TensorProduct/Basic.lean#L14-L19

I can claim that one!

[Yaël Dillies]

@Paul Lezeau, are you still working on this?

[Paul Lezeau]

Yaël Dillies said:

Paul Lezeau, are you still working on this?

Yep! But still somewhat WIP