Matrix.rank_diagonal
theorem Matrix.rank_diagonal :
∀ {m : Type u_2} {R : Type u_5} [inst : Field R] [inst_1 : Fintype m] [inst_2 : DecidableEq m]
[inst_3 : DecidableEq R] (w : m → R), (Matrix.diagonal w).rank = Fintype.card { i // w i ≠ 0 }
The theorem `Matrix.rank_diagonal` states that for any type `m` and any field `R`, given that `m` is a finite type and `m` and `R` have decidable equality, for any function `w` mapping from `m` to `R`, the rank of a matrix created by `Matrix.diagonal w` is equal to the count of non-zero elements in the set `{ i // w i ≠ 0 }`. In simpler terms, the rank of a diagonal matrix is equal to the count of non-zero elements on its main diagonal.
More concisely: For any finite type `m` and field `R` with decidable equality, the rank of a diagonal matrix `Matrix.diagonal w` over `R` is equal to the number of non-zero entries in `{ i // w i ≠ 0 }`.
|
Matrix.rank_eq_finrank_span_cols
theorem Matrix.rank_eq_finrank_span_cols :
∀ {m : Type u_2} {n : Type u_3} {R : Type u_5} [inst : Fintype n] [inst_1 : CommRing R] (A : Matrix m n R),
A.rank = FiniteDimensional.finrank R ↥(Submodule.span R (Set.range A.transpose))
The theorem `Matrix.rank_eq_finrank_span_cols` states that the rank of a matrix is equal to the rank of the space spanned by its columns. In more detail, for any matrix `A` with entries in a commutative ring `R` and indices `m` and `n` (where `n` is finite), the rank of `A` is equal to the finite dimension of the vector space spanned by the columns of `A`. Here, the span of the columns is considered as a submodule of the module of column vectors, and its rank is computed as a natural number, with the convention that it is `0` if the module has infinite rank.
More concisely: The rank of a matrix over a commutative ring equals the finite dimension of the submodule spanned by its columns.
|
Matrix.rank_mul_eq_left_of_isUnit_det
theorem Matrix.rank_mul_eq_left_of_isUnit_det :
∀ {m : Type u_2} {n : Type u_3} {R : Type u_5} [inst : Fintype n] [inst_1 : CommRing R] [inst_2 : DecidableEq n]
(A : Matrix n n R) (B : Matrix m n R), IsUnit A.det → (B * A).rank = B.rank
The theorem `Matrix.rank_mul_eq_left_of_isUnit_det` asserts that for any two matrices `A` and `B`, with `A` being a square matrix of any order, and `B` being a matrix indexed by some type `m` and `n`, over a commutative ring `R`, if the determinant of `A` is a unit (meaning it has an inverse), then the rank of the product of `B` and `A` (i.e., `B * A`) is equal to the rank of `B`. In other words, right multiplying by an invertible matrix does not change the rank of the original matrix. The theorem requires the existence of a finite type for `n`, a commutative ring structure on `R`, and decidability of equality for `n`.
More concisely: If matrix `A` is a square matrix over commutative ring `R` with invertible determinant, then the rank of matrix `B * A` equals the rank of matrix `B`.
|
Matrix.rank_submatrix_le
theorem Matrix.rank_submatrix_le :
∀ {m : Type u_2} {n : Type u_3} {R : Type u_5} [inst : Fintype n] [inst_1 : CommRing R]
[inst_2 : StrongRankCondition R] [inst_3 : Fintype m] (f : n → m) (e : n ≃ m) (A : Matrix m m R),
(A.submatrix f ⇑e).rank ≤ A.rank
This theorem states that for any matrix `A` with elements in a commutative ring `R` and indices from types `m` and `n`, and given a function `f` from `n` to `m` and a bijective function `e` (i.e., a permutation) from `n` to `m`, the rank of the submatrix of `A` obtained by taking a subset of the rows according to `f` and permuting the columns according to `e`, is less than or equal to the rank of the original matrix `A`. This result holds when `R` satisfies the Strong Rank Condition, and both `m` and `n` are finite types.
More concisely: For any matrix over a commutative ring satisfying the Strong Rank Condition with finite dimensions m and n, the rank of a submatrix obtained by row permutations and column permutations is less than or equal to the rank of the original matrix.
|
Matrix.rank_eq_finrank_span_row
theorem Matrix.rank_eq_finrank_span_row :
∀ {m : Type u_2} {n : Type u_3} {R : Type u_5} [inst : Fintype n] [inst_1 : LinearOrderedField R]
[inst_2 : Finite m] (A : Matrix m n R), A.rank = FiniteDimensional.finrank R ↥(Submodule.span R (Set.range A))
The theorem `Matrix.rank_eq_finrank_span_row` states that the rank of a matrix is equal to the rank of the space spanned by its rows. This is valid for any matrix `A` of type `Matrix m n R`, where `m` is the type of row indices, `n` is the type of column indices, and `R` is the type of entries, given that `n` is finite and `R` is a linearly ordered field, and `m` is finite. Note that the current formulation of this theorem is applicable to rational numbers (`ℚ`) and real numbers (`ℝ`), but a general proof that works for complex numbers (`ℂ`) is still needed.
More concisely: The rank of a finite matrix over a linearly ordered field equals the number of linearly independent rows.
|
Matrix.rank_conjTranspose
theorem Matrix.rank_conjTranspose :
∀ {m : Type u_2} {n : Type u_3} {R : Type u_5} [inst : Fintype n] [inst_1 : Fintype m] [inst_2 : Field R]
[inst_3 : PartialOrder R] [inst_4 : StarRing R] [inst_5 : StarOrderedRing R] (A : Matrix m n R),
A.conjTranspose.rank = A.rank
This theorem states that for any Matrix `A` with entries in a field `R`, where `R` has additional structures such as a partial order, a star-ring, and a star-ordered ring, and the rows are indexed by `m` and columns are indexed by `n` (both of which are finite types), the rank of the conjugate transpose of `A` is the same as the rank of `A` itself. The conjugate transpose of a matrix is obtained by taking the transpose of the matrix and then taking the complex conjugate of each entry. The rank of a matrix is a fundamental concept in linear algebra which refers to the maximum number of linearly independent row (or column) vectors in the matrix. The fact that the rank remains the same under the operation of taking the conjugate transpose is a useful property in various areas of mathematics.
More concisely: For any square matrix A over a field endowed with a partial order, star-ring, and star-ordered ring structures, the rank of A equals the rank of its conjugate transpose.
|
Matrix.rank_transpose
theorem Matrix.rank_transpose :
∀ {m : Type u_2} {n : Type u_3} {R : Type u_5} [inst : Fintype n] [inst_1 : Fintype m]
[inst_2 : LinearOrderedField R] (A : Matrix m n R), A.transpose.rank = A.rank
This theorem states that for any matrix `A` with entries in a linearly ordered field `R`, where the rows are indexed by some type `m` and the columns are indexed by some type `n` (both of which are assumed to be finite), the rank of the transpose of `A` is equal to the rank of `A` itself. Essentially, this theorem asserts that transposing a matrix does not change its rank.
More concisely: For any finite, square matrix `A` over a linearly ordered field, the rank of `A` equals the rank of its transpose.
|
Matrix.rank_mul_eq_right_of_isUnit_det
theorem Matrix.rank_mul_eq_right_of_isUnit_det :
∀ {m : Type u_2} {n : Type u_3} {R : Type u_5} [inst : Fintype n] [inst_1 : CommRing R] [inst_2 : Fintype m]
[inst_3 : DecidableEq m] (A : Matrix m m R) (B : Matrix m n R), IsUnit A.det → (A * B).rank = B.rank
The theorem `Matrix.rank_mul_eq_right_of_isUnit_det` states that for any two matrices `A` and `B`, where `A` is a square matrix and `B` is an arbitrary matrix, and the types of their elements (`R`) form a commutative ring, if the determinant of `A` is a unit (i.e., its determinant is invertible), then the rank of the product `A * B` is equal to the rank of `B`. This implies that left multiplying by an invertible matrix does not change the rank of the matrix. The types of the row and column indices of the matrices (`m` and `n` respectively) are finite and have a decidable equality.
More concisely: If `A` is a square matrix over a commutative ring with invertible determinant, then the rank of `A * B` equals the rank of `B`.
|
Matrix.rank_mul_le_left
theorem Matrix.rank_mul_le_left :
∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {R : Type u_5} [inst : Fintype n] [inst_1 : Fintype o]
[inst_2 : CommRing R] [inst_3 : StrongRankCondition R] (A : Matrix m n R) (B : Matrix n o R),
(A * B).rank ≤ A.rank
The theorem `Matrix.rank_mul_le_left` states that for any commutative ring `R` with a strong rank condition and any two matrices `A` and `B` with entries in `R`, where `A` has type `Matrix m n R` and `B` has type `Matrix n o R` (`m`, `n`, and `o` are types that index the rows and columns of the matrices, and `Fintype n` and `Fintype o` indicate that `n` and `o` are finite), the rank of the product `A * B` is less than or equal to the rank of `A`. In other words, the rank of the product of two matrices can never exceed the rank of the first matrix.
More concisely: The rank of the product of two matrices over a commutative ring with a strong rank condition is less than or equal to the rank of the first matrix.
|