mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(linear_algebra/ray): relation to linear independence

Open jsm28 opened this issue 3 years ago • 0 comments

Add lemmas that two vectors are linearly dependent if and only if they are in the same ray or one is in the same ray as the negation of the other (for a module over a linear_ordered_comm_ring with no_zero_smul_divisors).

Open in Gitpod

jsm28 avatar Aug 14 '22 19:08 jsm28