English
If the rows of a matrix M are linearly independent, then the rank of M equals the number of rows.
Русский
Если строки матрицы M линейно независимы, то ранг M равен числу строк.
LaTeX
$$$ \text{If } M\text{ has linearly independent rows, then } M\mathrm{rank} = |m|. $$$
Lean4
theorem _root_.LinearIndependent.rank_matrix [Field R] [Fintype m] {M : Matrix m n R} (h : LinearIndependent R M.row) :
M.rank = Fintype.card m := by
rw [M.rank_eq_finrank_span_row, linearIndependent_iff_card_eq_finrank_span.mp h, Set.finrank]