Row-reduced echelon forms

Stream: Is there code for X?

[Vivek Rajesh Joshi]

Have row-reduced echelon forms, and the algorithm to reduce matrices into this form, been formalised in Mathlib4? If so, where can I find the code?

[Kim Morrison]

Vivek Rajesh Joshi said:

Have row-reduced echelon forms, and the algorithm to reduce matrices into this form, been formalised in Mathlib4? If so, where can I find the code?

Doesn't the discussion following your previous question about Gaussian elimination already answer this in the negative?

[Vivek Rajesh Joshi]

Ohh okay thanks, that makes sense