Commit 2025-03-23 09:06 40de6ff4
View on Github →feat(LinearAlgebra/FiniteDimensional): add basisOfPiSpaceOfLinearIndependent (#22868)
Add a specialized version of basisOfLinearIndependentOfCardEqFinrank for the space ι → K. This has two advantages: it makes some proof shorter and it also works in the case ι empty.