mathlib
b3f602b9 - feat(linear_algebra/linear_independent): add variant of `exists_linear_independent` (#9708)

Commit

4 years ago

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

Author

ocfnash

Parents