Zulip Chat Archive
Stream: toric
Topic: Tensor linearly independent families
Paul Lezeau (Mar 09 2025 at 11:05):
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 (Mar 15 2025 at 20:54):
@Paul Lezeau, are you still working on this?
Paul Lezeau (Mar 15 2025 at 20:56):
Yaël Dillies said:
Paul Lezeau, are you still working on this?
Yep! But still somewhat WIP
Last updated: May 02 2025 at 03:31 UTC