Documentation

Mathlib.Data.Matrix.Rank

Rank of matrices #

The rank of a matrix A is defined to be the rank of range of the linear map corresponding to A. This definition does not depend on the choice of basis, see Matrix.rank_eq_finrank_range_toLin.

Main declarations #

noncomputable def Matrix.cRank {m : Type um} {n : Type un} {R : Type uR} [Semiring R] (A : Matrix m n R) :

The rank of a matrix, defined as the dimension of its column space, as a cardinal.

Equations
Instances For
    theorem Matrix.lift_cRank_submatrix_le {m : Type um} {m₀ : Type um₀} {n : Type un} {n₀ : Type un₀} {R : Type uR} [Semiring R] (A : Matrix m n R) (r : m₀m) (c : n₀n) :
    theorem Matrix.cRank_submatrix_le {n : Type un} {n₀ : Type un₀} {R : Type uR} [Semiring R] {m m₀ : Type um} (A : Matrix m n R) (r : m₀m) (c : n₀n) :

    A special case of lift_cRank_submatrix_le for when m₀ and m are in the same universe.

    theorem Matrix.cRank_le_card_height {m : Type um} {n : Type un} {R : Type uR} [Semiring R] [StrongRankCondition R] [Fintype m] (A : Matrix m n R) :
    theorem Matrix.cRank_le_card_width {m : Type um} {n : Type un} {R : Type uR} [Semiring R] [StrongRankCondition R] [Fintype n] (A : Matrix m n R) :
    noncomputable def Matrix.eRank {m : Type um} {n : Type un} {R : Type uR} [Semiring R] (A : Matrix m n R) :

    The rank of a matrix, defined as the dimension of its column space, as a term in ℕ∞.

    Equations
    Instances For
      theorem Matrix.eRank_toNat_eq_finrank {m : Type um} {n : Type un} {R : Type uR} [Semiring R] (A : Matrix m n R) :
      theorem Matrix.eRank_submatrix_le {m : Type um} {m₀ : Type um₀} {n : Type un} {n₀ : Type un₀} {R : Type uR} [Semiring R] (A : Matrix m n R) (r : m₀m) (c : n₀n) :
      theorem Matrix.eRank_le_card_width {m : Type um} {n : Type un} {R : Type uR} [Semiring R] [StrongRankCondition R] (A : Matrix m n R) :
      theorem Matrix.eRank_le_card_height {m : Type um} {n : Type un} {R : Type uR} [Semiring R] [StrongRankCondition R] (A : Matrix m n R) :
      noncomputable def Matrix.rank {m : Type um} {n : Type un} {R : Type uR} [Fintype n] [CommRing R] (A : Matrix m n R) :

      The rank of a matrix is the rank of its image.

      Equations
      Instances For
        @[simp]
        @[simp]
        @[simp]
        theorem Matrix.rank_zero {m : Type um} {n : Type un} {R : Type uR} [Fintype n] [CommRing R] [Nontrivial R] :
        rank 0 = 0
        @[simp]
        theorem Matrix.cRank_zero {R : Type uR} [CommRing R] {m : Type u_1} {n : Type u_2} [Nontrivial R] :
        cRank 0 = 0
        @[simp]
        theorem Matrix.eRank_zero {R : Type uR} [CommRing R] {m : Type u_1} {n : Type u_2} [Nontrivial R] :
        eRank 0 = 0
        theorem Matrix.rank_le_card_width {m : Type um} {n : Type un} {R : Type uR} [Fintype n] [CommRing R] [StrongRankCondition R] (A : Matrix m n R) :
        theorem Matrix.rank_le_width {R : Type uR} [CommRing R] [StrongRankCondition R] {m n : } (A : Matrix (Fin m) (Fin n) R) :
        A.rank n
        theorem Matrix.rank_mul_le_left {m : Type um} {n : Type un} {o : Type uo} {R : Type uR} [Fintype n] [Fintype o] [CommRing R] [StrongRankCondition R] (A : Matrix m n R) (B : Matrix n o R) :
        (A * B).rank A.rank
        theorem Matrix.rank_mul_le_right {m : Type um} {n : Type un} {o : Type uo} {R : Type uR} [Fintype n] [Fintype o] [CommRing R] [StrongRankCondition R] (A : Matrix m n R) (B : Matrix n o R) :
        (A * B).rank B.rank
        theorem Matrix.rank_mul_le {m : Type um} {n : Type un} {o : Type uo} {R : Type uR} [Fintype n] [Fintype o] [CommRing R] [StrongRankCondition R] (A : Matrix m n R) (B : Matrix n o R) :
        (A * B).rank A.rank B.rank
        theorem Matrix.rank_unit {n : Type un} {R : Type uR} [Fintype n] [CommRing R] [StrongRankCondition R] [DecidableEq n] (A : (Matrix n n R)ˣ) :
        theorem Matrix.rank_of_isUnit {n : Type un} {R : Type uR} [Fintype n] [CommRing R] [StrongRankCondition R] [DecidableEq n] (A : Matrix n n R) (h : IsUnit A) :
        @[simp]
        theorem Matrix.rank_mul_eq_left_of_isUnit_det {m : Type um} {n : Type un} {R : Type uR} [Fintype n] [CommRing R] [DecidableEq n] (A : Matrix n n R) (B : Matrix m n R) (hA : IsUnit A.det) :
        (B * A).rank = B.rank

        Right multiplying by an invertible matrix does not change the rank

        @[simp]
        theorem Matrix.rank_mul_eq_right_of_isUnit_det {m : Type um} {n : Type un} {R : Type uR} [Fintype n] [CommRing R] [Fintype m] [DecidableEq m] (A : Matrix m m R) (B : Matrix m n R) (hA : IsUnit A.det) :
        (A * B).rank = B.rank

        Left multiplying by an invertible matrix does not change the rank

        theorem Matrix.rank_submatrix_le {m : Type um} {n : Type un} {R : Type uR} [Fintype n] [CommRing R] [StrongRankCondition R] [Fintype m] (f : nm) (e : n m) (A : Matrix m m R) :
        (A.submatrix f e).rank A.rank

        Taking a subset of the rows and permuting the columns reduces the rank.

        theorem Matrix.rank_reindex {m : Type um} {m₀ : Type um₀} {n : Type un} {n₀ : Type un₀} {R : Type uR} [Fintype n] [CommRing R] [Fintype n₀] (em : m m₀) (en : n n₀) (A : Matrix m n R) :
        ((reindex em en) A).rank = A.rank
        @[simp]
        theorem Matrix.rank_submatrix {m : Type um} {m₀ : Type um₀} {n : Type un} {n₀ : Type un₀} {R : Type uR} [Fintype n] [CommRing R] [Fintype n₀] (A : Matrix m n R) (em : m₀ m) (en : n₀ n) :
        (A.submatrix em en).rank = A.rank
        @[simp]
        theorem Matrix.lift_cRank_submatrix {m : Type um} {m₀ : Type um₀} {n₀ : Type un₀} {R : Type uR} [CommRing R] {n : Type un} (A : Matrix m n R) (em : m₀ m) (en : n₀ n) :
        @[simp]
        theorem Matrix.cRank_submatrix {m : Type um} {n₀ : Type un₀} {R : Type uR} [CommRing R] {m₀ : Type um} {n : Type un} (A : Matrix m n R) (em : m₀ m) (en : n₀ n) :
        (A.submatrix em en).cRank = A.cRank

        A special case of lift_cRank_submatrix for when the row types are in the same universe.

        theorem Matrix.lift_cRank_reindex {m : Type um} {m₀ : Type um₀} {n₀ : Type un₀} {R : Type uR} [CommRing R] {n : Type un} (A : Matrix m n R) (em : m m₀) (en : n n₀) :
        theorem Matrix.cRank_reindex {m : Type um} {n₀ : Type un₀} {R : Type uR} [CommRing R] {m₀ : Type um} {n : Type un} (A : Matrix m n R) (em : m m₀) (en : n n₀) :
        ((reindex em en) A).cRank = A.cRank

        A special case of lift_cRank_reindex for when the row types are in the same universe.

        @[simp]
        theorem Matrix.eRank_submatrix {m : Type um} {m₀ : Type um₀} {n₀ : Type un₀} {R : Type uR} [CommRing R] {n : Type un} (A : Matrix m n R) (em : m₀ m) (en : n₀ n) :
        (A.submatrix em en).eRank = A.eRank
        theorem Matrix.eRank_reindex {m : Type um} {n₀ : Type un₀} {R : Type uR} [CommRing R] {m₀ : Type um} {n : Type un} (A : Matrix m n R) (em : m m₀) (en : n n₀) :
        ((reindex em en) A).eRank = A.eRank
        theorem Matrix.rank_eq_finrank_range_toLin {m : Type um} {n : Type un} {R : Type uR} [Fintype n] [CommRing R] [Finite m] [DecidableEq n] {M₁ : Type u_1} {M₂ : Type u_2} [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] (A : Matrix m n R) (v₁ : Basis m R M₁) (v₂ : Basis n R M₂) :
        A.rank = Module.finrank R (LinearMap.range ((toLin v₂ v₁) A))
        theorem Matrix.rank_le_card_height {m : Type um} {n : Type un} {R : Type uR} [Fintype n] [CommRing R] [Fintype m] [StrongRankCondition R] (A : Matrix m n R) :
        theorem Matrix.rank_le_height {R : Type uR} [CommRing R] [StrongRankCondition R] {m n : } (A : Matrix (Fin m) (Fin n) R) :
        A.rank m
        theorem Matrix.rank_eq_finrank_span_cols {m : Type um} {n : Type un} {R : Type uR} [Fintype n] [CommRing R] (A : Matrix m n R) :

        The rank of a matrix is the rank of the space spanned by its columns.

        @[simp]
        theorem Matrix.cRank_toNat_eq_rank {m : Type um} {n : Type un} {R : Type uR} [Fintype n] [CommRing R] (A : Matrix m n R) :
        @[simp]
        theorem Matrix.eRank_toNat_eq_rank {m : Type um} {n : Type un} {R : Type uR} [Fintype n] [CommRing R] (A : Matrix m n R) :
        theorem Matrix.rank_diagonal {m : Type um} {R : Type uR} [Field R] [Fintype m] [DecidableEq m] [DecidableEq R] (w : mR) :
        (diagonal w).rank = Fintype.card { i : m // w i 0 }

        The rank of a diagonal matrix is the count of non-zero elements on its main diagonal

        theorem Matrix.cRank_diagonal {m : Type um} {R : Type uR} [Field R] [DecidableEq m] (w : mR) :
        theorem Matrix.eRank_diagonal {m : Type um} {R : Type uR} [Field R] [DecidableEq m] (w : mR) :
        (diagonal w).eRank = {i : m | w i 0}.encard

        Lemmas about transpose and conjugate transpose #

        This section contains lemmas about the rank of Matrix.transpose and Matrix.conjTranspose.

        Unfortunately the proofs are essentially duplicated between the two; is a linearly-ordered ring but can't be a star-ordered ring, while is star-ordered (with open ComplexOrder) but not linearly ordered. For now we don't prove the transpose case for .

        TODO: the lemmas Matrix.rank_transpose and Matrix.rank_conjTranspose current follow a short proof that is a simple consequence of Matrix.rank_transpose_mul_self and Matrix.rank_conjTranspose_mul_self. This proof pulls in unnecessary assumptions on R, and should be replaced with a proof that uses Gaussian reduction or argues via linear combinations.

        theorem Matrix.rank_conjTranspose_mul_self {m : Type um} {n : Type un} {R : Type uR} [Fintype n] [Fintype m] [Field R] [PartialOrder R] [StarRing R] [StarOrderedRing R] (A : Matrix m n R) :
        @[simp]
        theorem Matrix.rank_conjTranspose {m : Type um} {n : Type un} {R : Type uR} [Fintype n] [Fintype m] [Field R] [PartialOrder R] [StarRing R] [StarOrderedRing R] (A : Matrix m n R) :

        TODO: prove this in greater generality.

        @[simp]
        theorem Matrix.rank_self_mul_conjTranspose {m : Type um} {n : Type un} {R : Type uR} [Fintype n] [Fintype m] [Field R] [PartialOrder R] [StarRing R] [StarOrderedRing R] (A : Matrix m n R) :
        theorem Matrix.rank_transpose_mul_self {m : Type um} {n : Type un} {R : Type uR} [Fintype n] [Fintype m] [LinearOrderedField R] (A : Matrix m n R) :
        @[simp]
        theorem Matrix.rank_transpose {m : Type um} {n : Type un} {R : Type uR} [Fintype n] [Field R] [Fintype m] (A : Matrix m n R) :
        @[simp]
        theorem Matrix.rank_self_mul_transpose {m : Type um} {n : Type un} {R : Type uR} [Fintype n] [LinearOrderedField R] [Fintype m] (A : Matrix m n R) :
        theorem Matrix.rank_eq_finrank_span_row {m : Type um} {n : Type un} {R : Type uR} [Fintype n] [Field R] [Finite m] (A : Matrix m n R) :

        The rank of a matrix is the rank of the space spanned by its rows.

        theorem LinearIndependent.rank_matrix {m : Type um} {n : Type un} {R : Type uR} [Fintype n] [Field R] [Fintype m] {M : Matrix m n R} (h : LinearIndependent R M) :
        theorem Matrix.rank_add_rank_le_card_of_mul_eq_zero {l : Type ul} {m : Type um} {n : Type un} {R : Type uR} [Fintype n] [Field R] [Finite l] [Fintype m] {A : Matrix l m R} {B : Matrix m n R} (hAB : A * B = 0) :