Commit 2017-12-08 17:29 fccc5d32
View on Github →refactor(algebra/linear_algebra): move zero_not_mem_of_linear_independent from vector_space to module (zero_ne_one should be a typeclass in Prop not in Type)
refactor(algebra/linear_algebra): move zero_not_mem_of_linear_independent from vector_space to module (zero_ne_one should be a typeclass in Prop not in Type)