Commit 2024-10-09 05:56 fef6814f

feat: Fintype instance for an extended family of linearly independent vectors (#17541) Given a family of linearly independent vectors $s \subset t$, one can get a linearly independent family which spans the submodule spanned by $t$ containing $s$. We add a Fintype instance for this family in the case where the span of $t$ is finite so as to be able to write sums over this type when manipulating bases indexed by it (typically Basis.extend and similar).