rank_matrix — Mathlib

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]

Похожие утверждения