Matrix.Pivot.mul_listTransvecRow_last_col
theorem Matrix.Pivot.mul_listTransvecRow_last_col :
∀ {𝕜 : Type u_3} [inst : Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) (i : Fin r ⊕ Unit),
(M * (Matrix.Pivot.listTransvecRow M).prod) i (Sum.inr ()) = M i (Sum.inr ())
The theorem `Matrix.Pivot.mul_listTransvecRow_last_col` states that for any matrix `M`, whose rows and columns are indexed by `Fin r ⊕ Unit` (a disjoint sum of finite ordinal numbers and a singleton set), over a field `𝕜`, and any row index `i`, the element in the last column of the row `i` remains unchanged when `M` is right-multiplied by the product of all matrices in the list of transvections `listTransvecRow M`. A transvection is a matrix that differs from the identity matrix by a rank-1 matrix. In other words, the operation of multiplying `M` by all the matrices produced by `listTransvecRow M` does not alter the elements of the last column of `M`.
More concisely: For any matrix M over a field with rows and columns indexed by Fin r ⊕ Unit, the last column of row i is invariant under right-multiplication by the product of all transvections in listTransvecRow M.
|
Matrix.Pivot.reindex_exists_list_transvec_mul_mul_list_transvec_eq_diagonal
theorem Matrix.Pivot.reindex_exists_list_transvec_mul_mul_list_transvec_eq_diagonal :
∀ {n : Type u_1} {p : Type u_2} {𝕜 : Type u_3} [inst : Field 𝕜] [inst_1 : DecidableEq n] [inst_2 : DecidableEq p]
[inst_3 : Fintype n] [inst_4 : Fintype p] (M : Matrix p p 𝕜) (e : p ≃ n),
(∃ L L' D,
(List.map Matrix.TransvectionStruct.toMatrix L).prod * (Matrix.reindexAlgEquiv 𝕜 e) M *
(List.map Matrix.TransvectionStruct.toMatrix L').prod =
Matrix.diagonal D) →
∃ L L' D,
(List.map Matrix.TransvectionStruct.toMatrix L).prod * M *
(List.map Matrix.TransvectionStruct.toMatrix L').prod =
Matrix.diagonal D
This theorem states that the reduction of a matrix to diagonal form by elementary operations is invariant under reindexing. Specifically, given a square matrix `M` with elements from a field `𝕜`, and indices from type `p`, if there exists lists `L` and `L'` and a function `D` such that the product of matrices generated by mapping `L` and `L'` via `Matrix.TransvectionStruct.toMatrix`, and multiplication with `M` that has been reindexed using an equivalence `e`, equals to the diagonal matrix defined by `D`, then there exists lists `L` and `L'` and a function `D` such that the product of matrices generated by mapping `L` and `L'` via `Matrix.TransvectionStruct.toMatrix`, and multiplication with `M`, equals the diagonal matrix defined by `D`. Here, `Matrix.TransvectionStruct.toMatrix` associates to a `transvection_struct` the corresponding transvection matrix, and `Matrix.diagonal` is the square matrix with diagonal elements defined by `D` and off-diagonal elements are zero.
More concisely: Given two square matrices `M` over a field, if `M` can be reduced to a diagonal matrix `D` via elementary operations using indices from type `p`, and if `M` is reindexed using an equivalence `e`, then `M` can still be reduced to the same diagonal matrix `D` using the same elementary operations on the reindexed matrix.
|
Matrix.Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal_induction
theorem Matrix.Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal_induction :
∀ {𝕜 : Type u_3} [inst : Field 𝕜] {r : ℕ},
(∀ (M : Matrix (Fin r) (Fin r) 𝕜),
∃ L₀ L₀' D₀,
(List.map Matrix.TransvectionStruct.toMatrix L₀).prod * M *
(List.map Matrix.TransvectionStruct.toMatrix L₀').prod =
Matrix.diagonal D₀) →
∀ (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜),
∃ L L' D,
(List.map Matrix.TransvectionStruct.toMatrix L).prod * M *
(List.map Matrix.TransvectionStruct.toMatrix L').prod =
Matrix.diagonal D
This theorem, `Matrix.Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal_induction`, describes an inductive step in the process of reducing matrices to diagonal form using elementary operations. In particular, it states that if one can reduce any size `r` matrix to diagonal form using the elementary operations represented as a product of matrices generated by transvection structures, then one can also reduce matrices of size `r+1` (represented as `Fin r ⊕ Unit` in Lean, an extra dimension added to the matrix) to diagonal form using the same methodology. Specifically, for any such matrix `M`, there exists lists of transvection structures `L` and `L'`, and a diagonal matrix `D`, such that the product of the matrices generated by `L` and `L'`, with `M` in the middle, equals `D`.
More concisely: Given a matrix `M` of size `r+1` and any reduction of a size `r` matrix to diagonal form using transvection structures, there exist lists of transvection structures `L` and `L'` such that the product of the matrices generated by `L`, `M`, and `L'` is a diagonal matrix.
|
Matrix.Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal_aux
theorem Matrix.Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal_aux :
∀ {𝕜 : Type u_3} [inst : Field 𝕜] (n : Type) [inst_1 : Fintype n] [inst_2 : DecidableEq n] (M : Matrix n n 𝕜),
∃ L L' D,
(List.map Matrix.TransvectionStruct.toMatrix L).prod * M *
(List.map Matrix.TransvectionStruct.toMatrix L').prod =
Matrix.diagonal D
This theorem states that for any square matrix `M` with entries from a field `𝕜` and indices from a finite type `n` with decidable equality, there exist lists `L` and `L'` of transvection structures and a function `D` such that when `D` is used to form a diagonal matrix, and `L` and `L'` are used to form lists of matrices (by applying the `toMatrix` function to each transvection structure in `L` and `L'`, and then taking the product of each list of matrices), the product of the matrix formed from `L`, `M`, and the matrix formed from `L'` is equal to the diagonal matrix formed from `D`. Essentially, it states that any matrix can be reduced to a diagonal form using elementary row and column operations, as represented by the transvection structures. This statement is formulated specifically for `Type 0` because it will be used in an induction argument using `Fin r`. The general version of this theorem, which follows from this one and reindexing, is `exists_list_transvec_mul_mul_list_transvec_eq_diagonal`.
More concisely: For any square matrix over a field with decidable equality and finite indices, there exist lists of transvection structures whose products with the matrix and its transpose, and the product of their diagonal matrices, are equal.
|
Matrix.diagonal_transvection_induction
theorem Matrix.diagonal_transvection_induction :
∀ {n : Type u_1} {𝕜 : Type u_3} [inst : Field 𝕜] [inst_1 : DecidableEq n] [inst_2 : Fintype n]
(P : Matrix n n 𝕜 → Prop) (M : Matrix n n 𝕜),
(∀ (D : n → 𝕜), (Matrix.diagonal D).det = M.det → P (Matrix.diagonal D)) →
(∀ (t : Matrix.TransvectionStruct n 𝕜), P t.toMatrix) → (∀ (A B : Matrix n n 𝕜), P A → P B → P (A * B)) → P M
This theorem is an induction principle for matrices based on transvections. The theorem states that if a certain property is true for all diagonal matrices and all transvections, and if this property is preserved under matrix multiplication, then this property holds true for all matrices.
More specifically, to prove that a property holds for a matrix `M`, it suffices to show: (1) the property holds for all diagonal matrices `D` such that the determinant of `D` is equal to the determinant of `M`, (2) the property holds for all transvections `t`, and (3) if the property holds for matrices `A` and `B`, then it also holds for the product of `A` and `B`. This version of the theorem is slightly more general and is particularly useful when dealing with the special linear group `SLₙ` or the general linear group `GLₙ`.
More concisely: If a property is preserves under matrix multiplication and holds for all diagonal matrices with equal determinant and all transvections, then it holds for all matrices in the general linear group.
|
Matrix.updateRow_eq_transvection
theorem Matrix.updateRow_eq_transvection :
∀ {n : Type u_1} {R : Type u₂} [inst : DecidableEq n] [inst_1 : CommRing R] (i j : n) [inst_2 : Finite n] (c : R),
Matrix.updateRow 1 i (1 i + c • 1 j) = Matrix.transvection i j c
The theorem `Matrix.updateRow_eq_transvection` states that for any types `n` and `R`, where `n` has decidable equality and `R` is a commutative ring, and given `i`, `j` of type `n` and `c` of type `R`, updating the `i`-th row of the identity matrix by adding `c` times the `j`-th row to the `i`-th row produces a transvection matrix. Here, a transvection matrix is defined as the identity matrix plus `c` at position `(i, j)`, and updating a row of a matrix means replacing that row with specified values. This theorem essentially provides a method to generate a transvection matrix from the identity matrix by a specific kind of row operation.
More concisely: For any commutative ring R and natural numbers i, j, the matrix obtained by updating the i-th row of the identity matrix in R^(n x n) with j-th row added c times is a transvection matrix.
|
Matrix.Pivot.listTransvecCol_mul_mul_listTransvecRow_last_col
theorem Matrix.Pivot.listTransvecCol_mul_mul_listTransvecRow_last_col :
∀ {𝕜 : Type u_3} [inst : Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜),
M (Sum.inr ()) (Sum.inr ()) ≠ 0 →
∀ (i : Fin r),
((Matrix.Pivot.listTransvecCol M).prod * M * (Matrix.Pivot.listTransvecRow M).prod) (Sum.inr ()) (Sum.inl i) =
0
The theorem `Matrix.Pivot.listTransvecCol_mul_mul_listTransvecRow_last_col` states that for any matrix `M` with entries in a field `𝕜` and dimensions indexed by the sum type of a finite set of cardinality `r` and a singleton set, if the bottom-right entry of `M` is not zero, then when you multiply `M` from the left by the product of the list of transvections given by `listTransvecCol M` and from the right by the product of the list of transvections given by `listTransvecRow M`, the result will have all entries in the last row (except for the last one) equal to zero. Here, a transvection is a particular type of elementary matrix used to perform Gaussian elimination.
More concisely: For any square matrix M of size (r+1) x (r+1) over a field with non-zero bottom-right entry, the product of M with the left transvection matrix obtained from its column pivots and the right transvection matrix obtained from its row pivots has all but the last entry in the last row equal to zero.
|
Matrix.Pivot.mul_listTransvecRow_last_col_take
theorem Matrix.Pivot.mul_listTransvecRow_last_col_take :
∀ {𝕜 : Type u_3} [inst : Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) (i : Fin r ⊕ Unit) {k : ℕ},
k ≤ r → (M * (List.take k (Matrix.Pivot.listTransvecRow M)).prod) i (Sum.inr ()) = M i (Sum.inr ())
This theorem states that for any matrix `M` with entries in a field `𝕜` and rows and columns indexed by `Fin r ⊕ Unit`, and for any index `i` and any natural number `k` less than or equal to `r`, multiplying `M` by the product of the first `k` matrices in `Matrix.Pivot.listTransvecRow M` does not change the last column of `M`. Here, `Matrix.Pivot.listTransvecRow M` is a list of transvection matrices (which represent simple row operations) designed to replace the last row of a matrix with zeroes. In simpler words, performing limited row operations as defined by `listTransvecRow` on `M` do not affect the last column of the original matrix `M`.
More concisely: For any matrix M with entries in a field and rows and columns indexed by Fin r ⊕ Unit, and for any index i and natural number k ≤ r, multiplying M on the left by the product of the first k transvection matrices in Matrix.Pivot.listTransvecRow M leaves the last column unchanged.
|
Matrix.Pivot.exists_list_transvec_mul_diagonal_mul_list_transvec
theorem Matrix.Pivot.exists_list_transvec_mul_diagonal_mul_list_transvec :
∀ {n : Type u_1} {𝕜 : Type u_3} [inst : Field 𝕜] [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n 𝕜),
∃ L L' D,
M =
(List.map Matrix.TransvectionStruct.toMatrix L).prod * Matrix.diagonal D *
(List.map Matrix.TransvectionStruct.toMatrix L').prod
The theorem `Matrix.Pivot.exists_list_transvec_mul_diagonal_mul_list_transvec` states that for any square matrix `M` over a field `𝕜`, with elements indexed by a finite and decidable type `n`, there exist lists `L` and `L'` of transvection structures and a function `D` such that `M` can be expressed as the product of the matrix representation of the transvections in `L`, the diagonal matrix corresponding to `D`, and the matrix representation of the transvections in `L'`. This mirrors the process of performing row operations to bring a matrix to diagonal form.
More concisely: Given a square matrix M over a field with finite and decidable index type, there exist lists L and L' of transvection structures and a diagonal function D such that M = T(L) * D * T(L') where T(L) denotes the matrix representation of the transvections in L.
|
Matrix.Pivot.isTwoBlockDiagonal_listTransvecCol_mul_mul_listTransvecRow
theorem Matrix.Pivot.isTwoBlockDiagonal_listTransvecCol_mul_mul_listTransvecRow :
∀ {𝕜 : Type u_3} [inst : Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜),
M (Sum.inr ()) (Sum.inr ()) ≠ 0 →
((Matrix.Pivot.listTransvecCol M).prod * M * (Matrix.Pivot.listTransvecRow M).prod).IsTwoBlockDiagonal
This theorem states that for any field `𝕜` and a given matrix `M` with elements from field `𝕜` and dimension `r`, if the bottom-right element of the matrix `M` is not zero, then multiplying `M` from the left with the product of all matrices in the function `listTransvecCol M` and from the right with the product of all matrices in the function `listTransvecRow M` will transform `M` into a block-diagonal form. A block-diagonal matrix is a square matrix in which the main diagonal consists of square blocks and all elements outside these blocks are zero.
More concisely: If a matrix `M` in a field `𝕜` of dimension `r` has a non-zero bottom-right element, then left multiplication by the transposed columns matrices in `listTransvecCol M` and right multiplication by the transposed rows matrices in `listTransvecRow M` results in a block-diagonal matrix.
|
Matrix.Pivot.listTransvecCol_mul_last_col
theorem Matrix.Pivot.listTransvecCol_mul_last_col :
∀ {𝕜 : Type u_3} [inst : Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜),
M (Sum.inr ()) (Sum.inr ()) ≠ 0 →
∀ (i : Fin r), ((Matrix.Pivot.listTransvecCol M).prod * M) (Sum.inl i) (Sum.inr ()) = 0
The theorem `Matrix.Pivot.listTransvecCol_mul_last_col` states that for a matrix `M` with entries in a field `𝕜`, and the rows and columns indexed by `Fin r ⊕ Unit`, if the last entry of the last column of `M` is not zero, then multiplying `M` on the left by the product of all matrices in the list produced by the function `Matrix.Pivot.listTransvecCol M` results in a matrix where all coefficients in the last column, except for the last one, are zero. In other words, all the entries in the last column (except for the last row) of the resulting matrix will be zero.
More concisely: If `M` is an `r × (r + 1)` matrix with entries in a field and the last entry of its last column is nonzero, then left-multiplying `M` by the product of the transvectors of the first `r` columns of `M` results in a matrix with zeros in all entries of the last column but the last row.
|
Matrix.Pivot.listTransvecCol_mul_mul_listTransvecRow_last_row
theorem Matrix.Pivot.listTransvecCol_mul_mul_listTransvecRow_last_row :
∀ {𝕜 : Type u_3} [inst : Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜),
M (Sum.inr ()) (Sum.inr ()) ≠ 0 →
∀ (i : Fin r),
((Matrix.Pivot.listTransvecCol M).prod * M * (Matrix.Pivot.listTransvecRow M).prod) (Sum.inl i) (Sum.inr ()) =
0
This theorem states that for a given matrix `M` over a field `𝕜` with `r` number of rows and columns, if the entry at the last row and column of `M` is non-zero, then after multiplying `M` from the left with the product of all matrices in `listTransvecCol M` and from the right with the product of all matrices in `listTransvecRow M`, any coefficient in the last column (except the last one) of the resulting matrix will be 0. This means multiplying by the transvections in these lists effectively eliminates all coefficients in the last column except the last one.
More concisely: For a matrix M over a field with a non-zero entry at the last row and column, multiplying M from the left with the product of all transposed column matrices and from the right with the product of all transposed row matrices eliminates all coefficients in the last column except the last one.
|
Matrix.Pivot.exists_isTwoBlockDiagonal_list_transvec_mul_mul_list_transvec
theorem Matrix.Pivot.exists_isTwoBlockDiagonal_list_transvec_mul_mul_list_transvec :
∀ {𝕜 : Type u_3} [inst : Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜),
∃ L L',
((List.map Matrix.TransvectionStruct.toMatrix L).prod * M *
(List.map Matrix.TransvectionStruct.toMatrix L').prod).IsTwoBlockDiagonal
The theorem `Matrix.Pivot.exists_isTwoBlockDiagonal_list_transvec_mul_mul_list_transvec` asserts that given a field `𝕜` and a positive integer `r`, for any matrix `M` of size `(r + 1) × (r + 1)` with entries in `𝕜`, there exist two lists `L` and `L'` of transvection structures such that when we construct matrices from these transvection structures, the product of the list `L`'s matrices, the matrix `M`, and the product of the list `L'`'s matrices, in that order, results in a block-diagonal matrix. Here, a block-diagonal matrix is one that can be viewed as a matrix of matrices, where the off-diagonal blocks are zero.
More concisely: Given a field `𝕜` and a positive integer `r`, there exist lists `L` and `L'` of transvection structures of size `r+1` over `𝕜` such that the product of the matrices constructed from `L`, `M`, and the matrices constructed from `L'` in that order is a block-diagonal matrix.
|
Matrix.diagonal_transvection_induction_of_det_ne_zero
theorem Matrix.diagonal_transvection_induction_of_det_ne_zero :
∀ {n : Type u_1} {𝕜 : Type u_3} [inst : Field 𝕜] [inst_1 : DecidableEq n] [inst_2 : Fintype n]
(P : Matrix n n 𝕜 → Prop) (M : Matrix n n 𝕜),
M.det ≠ 0 →
(∀ (D : n → 𝕜), (Matrix.diagonal D).det ≠ 0 → P (Matrix.diagonal D)) →
(∀ (t : Matrix.TransvectionStruct n 𝕜), P t.toMatrix) →
(∀ (A B : Matrix n n 𝕜), A.det ≠ 0 → B.det ≠ 0 → P A → P B → P (A * B)) → P M
This theorem states the following principle for induction on invertible matrices using transvections: Given a certain property `P` and a matrix `M` with non-zero determinant over a field `𝕜`, if `P` holds for all invertible diagonal matrices with non-zero determinant, if `P` holds for all transvections, and if `P` is preserved under multiplication of invertible matrices with non-zero determinant, then `P` holds for `M`. In other words, this theorem provides a way to prove a property for all invertible matrices by showing it holds for simpler classes of matrices (diagonal matrices and transvections), and is preserved under multiplication. This theorem essentially formalizes the fact that invertible matrices can be generated by invertible diagonal matrices and transvections.
More concisely: Given a property `P` and a matrix `M` with non-zero determinant over a field `𝕜`, if `P` holds for all invertible diagonal matrices and all transvections, then `P` holds for `M` if `P` is preserved under multiplication.
|
Matrix.Pivot.mul_listTransvecRow_last_row
theorem Matrix.Pivot.mul_listTransvecRow_last_row :
∀ {𝕜 : Type u_3} [inst : Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜),
M (Sum.inr ()) (Sum.inr ()) ≠ 0 →
∀ (i : Fin r), (M * (Matrix.Pivot.listTransvecRow M).prod) (Sum.inr ()) (Sum.inl i) = 0
The theorem `Matrix.Pivot.mul_listTransvecRow_last_row` states that for any field `𝕜`, any natural number `r`, and any matrix `M` indexed by `Fin r ⊕ Unit` and with entries in `𝕜`, if the element at the bottom right corner of `M` is not zero, then when we right-multiply `M` by the product of the list of matrices given by `Matrix.Pivot.listTransvecRow M`, all the entries in the last row of the resulting matrix, excluding the last one, will be zero. In other words, all the coefficients in the last row but the last one are eliminated when multiplying by all the matrices in `Matrix.Pivot.listTransvecRow M`.
More concisely: If `M` is an `r × r` matrix over a field with a non-zero entry at the bottom-right corner, then multiplying `M` by the product of the last `r-1` transposed row reduction matrices from `Matrix.Pivot.listTransvecRow M` results in a matrix with all but the last entry in the last row being zero.
|
Matrix.Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal
theorem Matrix.Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal :
∀ {n : Type u_1} {𝕜 : Type u_3} [inst : Field 𝕜] [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n 𝕜),
∃ L L' D,
(List.map Matrix.TransvectionStruct.toMatrix L).prod * M *
(List.map Matrix.TransvectionStruct.toMatrix L').prod =
Matrix.diagonal D
This theorem states that for any matrix `M` over a field `𝕜`, where the field has decidable equality and finiteness property, there exist lists `L` and `L'` of transvection structures and a diagonal matrix `D` such that the product of the matrices corresponding to `L`, `M`, and the matrices corresponding to `L'` equals `D`. In other words, any matrix can be reduced to a diagonal form by a sequence of elementary row and column operations, which are represented by transvections. These operations do not change the determinant of the matrix.
More concisely: Given a matrix M over a decidably equal and finite field, there exist lists L and L' of transvection structures such that M is equivalent to their product with a diagonal matrix.
|
Matrix.Pivot.exists_isTwoBlockDiagonal_of_ne_zero
theorem Matrix.Pivot.exists_isTwoBlockDiagonal_of_ne_zero :
∀ {𝕜 : Type u_3} [inst : Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜),
M (Sum.inr ()) (Sum.inr ()) ≠ 0 →
∃ L L',
((List.map Matrix.TransvectionStruct.toMatrix L).prod * M *
(List.map Matrix.TransvectionStruct.toMatrix L').prod).IsTwoBlockDiagonal
This theorem states that for a given field `𝕜` and a positive integer `r`, if we have a Matrix `M` with entries from `𝕜` and row/column indices from the sum type of `Fin r` and `Unit`, then if the entry of `M` at the position corresponding to `Sum.inr ()`(which represents the last row and column) is non-zero, there exist two lists of `TransvectionStruct`, say `L` and `L'`, such that when we apply the product of the transvection matrices corresponding to `L` and `L'` to `M` from the left and right respectively, the resulting matrix is block-diagonal with two blocks.
Here, `Matrix.TransvectionStruct` is a structure representing a transvection, which is a particular type of elementary matrix used in matrix computations. This theorem is particularly useful in algorithms related to the reduction of matrices to simpler forms.
More concisely: Given a field `𝕜`, a positive integer `r`, and a matrix `M` over `𝕜` with dimensions `r x r`, if the last entry of `M` is non-zero, then there exist lists `L` and `L'` of transvection matrices such that `M` multiplied from the left by the matrices in `L` and from the right by the matrices in `L'` results in a block-diagonal matrix.
|
Matrix.Pivot.listTransvecCol_mul_last_row_drop
theorem Matrix.Pivot.listTransvecCol_mul_last_row_drop :
∀ {𝕜 : Type u_3} [inst : Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) (i : Fin r ⊕ Unit) {k : ℕ},
k ≤ r → ((List.drop k (Matrix.Pivot.listTransvecCol M)).prod * M) (Sum.inr ()) i = M (Sum.inr ()) i
This theorem states that for any field `𝕜` and any natural number `r`, and given a matrix `M` whose rows and columns are indexed by the sum type of `Fin r` and `Unit`, and an index `i` of the same type, for any natural number `k` less than or equal to `r`, the act of multiplying `M` by the product of the list obtained by dropping the first `k` elements from the list of transvection matrices (as defined by `listTransvecCol M`) does not change the last row of `M`. In other words, the entries in the last row of the resulting matrix are the same as those in the original matrix `M`.
More concisely: For any field `𝕜`, natural number `r`, matrix `M` indexed by `Fin r x Unit`, and natural number `k < r`, the product of `M` and the list of transvection matrices obtained by dropping the first `k` elements does not alter the last row of `M`.
|
Matrix.Pivot.listTransvecCol_mul_last_row
theorem Matrix.Pivot.listTransvecCol_mul_last_row :
∀ {𝕜 : Type u_3} [inst : Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) (i : Fin r ⊕ Unit),
((Matrix.Pivot.listTransvecCol M).prod * M) (Sum.inr ()) i = M (Sum.inr ()) i
The theorem `Matrix.Pivot.listTransvecCol_mul_last_row` states that for any matrix `M` with entries in a field `𝕜` and indexed by the sum type of a finite set of size `r` and a single element set, and for any index `i` of the same type, the result of multiplying `M` on the left by the product of all matrices in the list generated by `listTransvecCol M` (each of which is a transvection matrix aimed to replace the last column of `M` with zeroes) does not alter the last row of `M`. In other words, the last row of the original matrix `M` remains the same even after the left multiplication by the transvection matrices.
More concisely: For any matrix $M$ over a field and indexed by a finite sum type, and for any index $i$, the last row of $M$ is invariant under left multiplication by the list of transvection matrices obtained from $M$ by replacing its last column with zeroes.
|