mathlib3
3046436c - chore(linear_algebra/linear_independent): make a binding explicit in ne_zero (#5494)

Commit

5 years ago

chore(linear_algebra/linear_independent): make a binding explicit in ne_zero (#5494) Resubmitting #5479 from within the mathlib repo.

Author

Julian

Parents