Commit 2023-12-17 14:38 af42783d
View on Github →feat: A lin. indep. family of vectors in a fin. dim. space is finite (#9103)
This is just a repackaging of existing lemmas, except that the correct name is already taken by the Set version, so we fix that too.
From LeanAPAP