linearly independent

Stream: maths

[Sebastien Gouezel]

Is there a lemma telling me that, in a real vector space with dimension at least 2, given a nonzero vector x, I can find a vector y such that ![x, y] is linearly independent?

[Eric Wieser]

Maybe we have it more generally that if you have a set of n independent vectors you can extend it with finrank V - n more?

[Markus Himmel]

That's basically docs#Basis.extend

[Scott Morrison]

But having the special case of going from 1 to 2 seems particularly useful!