Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-15 16:38 b3f602b9

View on Github →

feat(linear_algebra/linear_independent): add variant of exists_linear_independent (#9708) Formalized as part of the Sphere Eversion project.

Estimated changes

modified theorem exists_linear_independent