Row space computations

Stream: Is there code for X?

[Vivek Rajesh Joshi]

In Linear Algebra by Hoffman and Kunze, there's a section on certain computations regarding the rows of a matrix. It describes algorithms for finding their linear dependency and what kind of vectors belong in the row space. Does this already exist in Mathlib4?

[Kim Morrison]

No; typically you're not going to find a one-to-one correspondence between material in elementary textbooks and the material in Mathlib.