Extract a basis from a spanning family

Stream: Is there code for X?

[Etienne Marion]

Hi! Given a family of vectors spanning the space, how do I extract a basis contained in this family please?

[Riccardo Brasca]

docs#Basis.mk ?

[Riccardo Brasca]

no sorry

[Riccardo Brasca]

We have a quite a few results like docs#exists_linearIndependent

[Riccardo Brasca]

If look for "maximal in Mathlib.LinearAlgebra.Basis there must be a way of getting a basis, but I am not sure which one is the quickest

[Riccardo Brasca]

The fact that it is not literally there makes me think that this can usually be avoided. But of course this may be not the case for you.

[Etienne Marion]

Thanks for your answer, I'll see what I can do with that. I haven't given it a great deal of thought yet because I assumed the literal statement would exist, but I suppose I'll be able to go around it.

[Riccardo Brasca]

well, it is docs#LinearIndependent.extend applied to the empty set I think

[Riccardo Brasca]

adds vectors to a linear independent set s ⊆ t until it spans all elements of t.

[Etienne Marion]

Ah yes, this should to the trick, thanks!

[Edward van de Meent]

a bit late, but if you already know your family is independent, Basis.span might be what you want