Commit 2024-10-08 09:15 196892df

feat: extend a linearly independent family to a basis contained in a set spanning the space (#17102) If s is a family of linearly independent vectors contained in a set t spanning V, extendLe is a basis of V containing s and contained in t. Specialize it for the case where s is empty.