Formalization of rank of system of linear equations

Stream: mathlib4

[Sham S]

Hi all, I see in the docs/undergrad.yaml the rank of system of linear equations on line 33 has no theorem/def associated with it. If there's no one working on it can I take it up?

[Oliver Nash]

I think this is only missing in the sense that Mathlib hasn't got an atomic name for this number. For example all of the following works:

import Mathlib.LinearAlgebra.Matrix.Rank

variable {R n m : Type*} [CommRing R] [Fintype m] [Fintype n] (A : Matrix m n R)

#check Matrix.rank -- This exists
#check Module.finrank R <| LinearMap.ker A.mulVecLin