Matrix.det_pow
theorem Matrix.det_pow :
∀ {m : Type u_1} [inst : DecidableEq m] [inst_1 : Fintype m] {R : Type v} [inst_2 : CommRing R] (M : Matrix m m R)
(n : ℕ), (M ^ n).det = M.det ^ n
This theorem states that for any given square matrix `M` with entries from a commutative ring `R`, and for any natural number `n`, the determinant of the matrix `M` raised to the power `n` (i.e., `M` multiplied with itself `n` times) is equal to the determinant of `M` itself raised to the power of `n`. Here the matrix `M` is defined over a type `m`, which has decidable equality and is finite.
More concisely: For any square matrix `M` over a commutative ring `R` with decidable equality and finite dimension, the determinant of `M` raised to the power `n` equals the determinant of `M` raised to the power `n`. In other words, `det(M^n) = det(M)^n`.
|
Matrix.det_succ_column
theorem Matrix.det_succ_column :
∀ {R : Type v} [inst : CommRing R] {n : ℕ} (A : Matrix (Fin n.succ) (Fin n.succ) R) (j : Fin n.succ),
A.det = Finset.univ.sum fun i => (-1) ^ (↑i + ↑j) * A i j * (A.submatrix i.succAbove j.succAbove).det
The theorem `Matrix.det_succ_column` states that for any commutative ring `R` and any natural number `n`, given an `(n+1)×(n+1)` matrix `A` with entries from `R`, the determinant of `A` can be computed using the Laplacian expansion along column `j`. More specifically, it is the sum over all rows `i` in `A` of `(-1)^(i+j) * A(i, j) * det(A')`, where `A'` is the submatrix of `A` obtained by removing row `i` and column `j`. Here `Finset.univ` is the set of all rows in `A`, and `i.succAbove` and `j.succAbove` denote the successor functions of `i` and `j`, respectively.
More concisely: For any commutative ring R and natural number n, the determinant of an (n+1)×(n+1) matrix A over R can be computed as the sum over all i in the set of rows of A, of (-1) ^ (i+j) * A(i, j) * determinant of the submatrix obtained by removing row i and column j from A.
|
Matrix.det_fin_three
theorem Matrix.det_fin_three :
∀ {R : Type v} [inst : CommRing R] (A : Matrix (Fin 3) (Fin 3) R),
A.det =
A 0 0 * A 1 1 * A 2 2 - A 0 0 * A 1 2 * A 2 1 - A 0 1 * A 1 0 * A 2 2 + A 0 1 * A 1 2 * A 2 0 +
A 0 2 * A 1 0 * A 2 1 -
A 0 2 * A 1 1 * A 2 0
This theorem describes the calculation of the determinant of a 3x3 matrix. For any 3x3 matrix `A` whose entries are in a commutative ring `R`, the determinant of `A` is equal to a particular combination of its entries:
`A 0 0 * A 1 1 * A 2 2 - A 0 0 * A 1 2 * A 2 1 - A 0 1 * A 1 0 * A 2 2 + A 0 1 * A 1 2 * A 2 0 + A 0 2 * A 1 0 * A 2 1 - A 0 2 * A 1 1 * A 2 0`.
This is the standard formula for the determinant of a 3x3 matrix, expressed as a sum and difference of products of entries of the matrix.
More concisely: The determinant of a 3x3 matrix over a commutative ring is equal to the sum and difference of certain products of its entries, as given by the standard formula: `|A| = A.01.22 - A.01.21 + A.00.21 - A.02.11 + A.02.12 - A.02.21 + A.00.11*A.22 - A.00.12*A.21 + A.01.12*A.20`.
|
Matrix.det_zero_of_column_eq
theorem Matrix.det_zero_of_column_eq :
∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {M : Matrix n n R}
{i j : n}, i ≠ j → (∀ (k : n), M k i = M k j) → M.det = 0
This theorem states that for any square matrix `M` (of any size `n` and entries in a commutative ring `R`), if there exist two distinct columns `i` and `j` such that every entry in column `i` is equal to the corresponding entry in column `j`, then the determinant of `M` is zero. The requirement that `i` and `j` be different is expressed by `i ≠ j`, and the condition that the entries in the two columns are equal is expressed by `∀ (k : n), M k i = M k j`. The theorem uses a decidability condition on the equality of elements of type `n` and assumes that `n` forms a finite type. In essence, the theorem captures the fact that determinant is a function that detects linear dependencies among the columns of a matrix: if two columns are equal, they are linearly dependent, and thus the determinant is zero.
More concisely: For any square matrix over a commutative ring with finite index type, if there exist distinct columns with identical entries, then the determinant is zero.
|
Matrix.det_mul_left_comm
theorem Matrix.det_mul_left_comm :
∀ {m : Type u_1} [inst : DecidableEq m] [inst_1 : Fintype m] {R : Type v} [inst_2 : CommRing R]
(M N P : Matrix m m R), (M * (N * P)).det = (N * (M * P)).det
The theorem `Matrix.det_mul_left_comm` states that for any type `m` with decidable equality and finite elements, and for any type `R` that forms a commutative ring, the determinant of the product of three square matrices `M`, `N`, and `P` (with elements in `R` and indices in `m`) is not affected by a left-commutative multiplication rearrangement. That is, the determinant of `M` multiplied by (`N` multiplied by `P`) equals the determinant of `N` multiplied by (`M` multiplied by `P`). This expresses a left-commutative property of matrix multiplication with respect to the determinant operation.
More concisely: For matrices `M`, `N`, and `P` of equal size over a commutative ring `R` with decidable equality and finite elements, the determinant of `M` multiplied by the determinant of `N` times the determinant of `P` equals the determinant of `N` multiplied by the determinant of `M` times the determinant of `P`.
|
Matrix.det_succ_column_zero
theorem Matrix.det_succ_column_zero :
∀ {R : Type v} [inst : CommRing R] {n : ℕ} (A : Matrix (Fin n.succ) (Fin n.succ) R),
A.det = Finset.univ.sum fun i => (-1) ^ ↑i * A i 0 * (A.submatrix i.succAbove Fin.succ).det
This theorem states the Laplacian expansion of the determinant of an `n+1` by `n+1` matrix along column 0. Given a commutative ring `R`, a natural number `n`, and a matrix `A` with entries in `R` and dimensions `n+1` by `n+1`, the determinant of `A` equals the sum, over the universal finite set (which is implied from the assumption that `Fin n.succ` is a finite type), of the product of `(-1)` raised to the power of the row index, the element at the i-th row and 0-th column of `A`, and the determinant of the submatrix of `A` obtained by deleting the i-th row and advancing all remaining rows by one index. This corresponds to the expansion of the determinant along the first column in the algebraic computation of determinants.
More concisely: The determinant of an `(n+1)` by `(n+1)` matrix `A` over a commutative ring `R` is equal to the sum, over all `i` in `Fin (n+1)`, of `(-1)^i` times the product of the `i`-th row's first element and the determinant of the submatrix obtained by deleting the `i`-th row and advancing all remaining rows, where `Fin` is the type of finite natural numbers.
|
Matrix.det_neg_eq_smul
theorem Matrix.det_neg_eq_smul :
∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (A : Matrix n n R),
(-A).det = (-1) ^ Fintype.card n • A.det
This theorem, `Matrix.det_neg_eq_smul`, states that for any square matrix `A` with entries in a commutative ring `R`, and indices from a finite set `n` with decidable equality, the determinant of the negated matrix `-A` is equal to the determinant of `A` multiplied by the `n`th power of `-1`. The power of `-1` is determined by the cardinality of the set `n`, i.e., the number of elements in the set `n`, which is also the dimension of the square matrix `A`.
More concisely: For any square matrix `A` of dimension `n` over a commutative ring `R` with decidable equality, the determinant of `-A` equals the negative of the determinant of `A` raised to the power of `n`.
|
Matrix.det_eq_zero_of_row_eq_zero
theorem Matrix.det_eq_zero_of_row_eq_zero :
∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {A : Matrix n n R}
(i : n), (∀ (j : n), A i j = 0) → A.det = 0
The theorem `Matrix.det_eq_zero_of_row_eq_zero` states that for any matrix `A` with entries in a commutative ring `R`, whose rows and columns are indexed by a type `n` that has decidable equality and is a finite type, if all the elements in a particular row `i` of `A` are zero, then the determinant of matrix `A` is zero. This is a formal statement of a well-known result in linear algebra, which says that if a matrix has a row of all zeros, its determinant is zero.
More concisely: If matrix `A` over commutative ring `R` with decidable equality and finite index type `n` has a zero row, then its determinant is zero.
|
Matrix.det_mul_row
theorem Matrix.det_mul_row :
∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (v : n → R)
(A : Matrix n n R), (Matrix.of fun i j => v j * A i j).det = (Finset.univ.prod fun i => v i) * A.det
This theorem in Lean 4 is asserting that for a given matrix `A` with elements of a commutative ring `R` and indices `n` (for which equality is decidable and the set of indices is finite), if we multiply each row of the matrix by a certain value `v i`, the determinant of the resulting matrix is equal to the product of all the `v i`s times the determinant of the original matrix `A`. In mathematical terms, given a matrix $A$ and a vector $v$ in $R^n$, the determinant of the matrix resulting from multiplying the $i$-th row of $A$ by the $i$-th component of $v$ is equal to $(v_1 * v_2 * ... * v_n) * det(A)$, where $v_i$ represents the $i$-th component of the vector $v$.
More concisely: For a matrix $A$ with determinant $det(A)$ over a commutative ring $R$ and finite indices $n$, the determinant of the matrix obtained by multiplying each row $i$ by the corresponding component $v\_i$ of vector $v$ in $R^n$ is equal to the product $(v\_1 * v\_2 * ... * v\_n) * det(A)$.
|
Matrix.det_submatrix_equiv_self
theorem Matrix.det_submatrix_equiv_self :
∀ {m : Type u_1} {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
[inst_3 : Fintype m] {R : Type v} [inst_4 : CommRing R] (e : n ≃ m) (A : Matrix m m R),
(A.submatrix ⇑e ⇑e).det = A.det
This theorem states that for any given square matrix `A` with entries in a commutative ring `R`, and for any equivalence between the indices of its rows and columns, the determinant of the submatrix obtained by permuting the rows and columns of `A` according to this equivalence is equal to the determinant of `A` itself. In other words, rearranging the rows and columns of a square matrix in the same manner does not change the determinant of the matrix.
More concisely: For any square matrix `A` over a commutative ring `R` and any equivalence of its indices, the determinant of the permuted submatrix is equal to the determinant of `A`.
|
Matrix.det_fin_one
theorem Matrix.det_fin_one : ∀ {R : Type v} [inst : CommRing R] (A : Matrix (Fin 1) (Fin 1) R), A.det = A 0 0 := by
sorry
This theorem, `Matrix.det_fin_one`, states that for any given type `R` that forms a commutative ring (denoted by `CommRing R`), the determinant of a 1x1 matrix `A` with entries in `R` (expressed as `Matrix (Fin 1) (Fin 1) R`) is equal to the single entry of the matrix, i.e., `A 0 0`. In other words, the determinant of a 1x1 matrix is the element itself.
More concisely: The determinant of a 1x1 matrix equals the matrix's unique entry.
|
Matrix.det_eq_of_forall_row_eq_smul_add_const
theorem Matrix.det_eq_of_forall_row_eq_smul_add_const :
∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {A B : Matrix n n R}
(c : n → R) (k : n), c k = 0 → (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det
This theorem states that for any square matrix `A` and `B` of size `n x n` over a commutative ring `R`, if a row of `A` is the sum of a row of `B` and a scalar multiple of another row of `B` (with the scalar being zero for the row itself), then the determinants of `A` and `B` are the same. Specifically, if for some `k` in `n` and a function `c` from `n` to `R` with `c(k) = 0`, each entry `A i j` is equal to `B i j` plus `c(i)` times `B k j` for all `i` and `j`, then the determinant of `A` equals the determinant of `B`. This reflects the fact that the determinant of a matrix remains unchanged by adding multiples of one row to another.
More concisely: If two square matrices of size `n x n` over a commutative ring have a row of the first equal to the sum of a row of the second and a scalar multiple of another row of the second, then they have equal determinants.
|
Matrix.det_zero_of_row_eq
theorem Matrix.det_zero_of_row_eq :
∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {M : Matrix n n R}
{i j : n}, i ≠ j → M i = M j → M.det = 0
The theorem `Matrix.det_zero_of_row_eq` states that for any matrix `M` with entries from a commutative ring `R`, whose rows are indexed by a finite type `n` (with decidable equality), if there exist two distinct indices `i` and `j` such that the `i`th row and `j`th row of `M` are equal, then the determinant of the matrix `M` is zero.
More concisely: If a square matrix over a commutative ring with decidable equality has two equal rows, then its determinant is zero.
|
Matrix.det_succ_row_zero
theorem Matrix.det_succ_row_zero :
∀ {R : Type v} [inst : CommRing R] {n : ℕ} (A : Matrix (Fin n.succ) (Fin n.succ) R),
A.det = Finset.univ.sum fun j => (-1) ^ ↑j * A 0 j * (A.submatrix Fin.succ j.succAbove).det
The theorem `Matrix.det_succ_row_zero` states that for any commutative ring `R` and a natural number `n`, the determinant of an `(n+1) x (n+1)` matrix with entries from `R` can be computed using the Laplacian expansion along the first row. Specifically, the determinant `A.det` of the matrix `A` is the sum over all `j` in the universal finite set (which corresponds to all valid column indices), of the product of `(-1) ^ j`, the element at the first row and `j`th column of `A` (denoted as `A 0 j`), and the determinant of the submatrix obtained by removing the first row and `j`th column from `A`. The `Fin.succ` and `j.succAbove` operations are used to increment the row and column indices, respectively, for the submatrix computation.
More concisely: For any commutative ring R and an (n+1)x(n+1) matrix A over R, the determinant of A is equal to the sum over j in [1,n+1] of (-1)^j * A(0,j) * det(A \ [0] (j : Fin (n+1))) where det(B) denotes the determinant of the matrix B and A[0] is the first row of A.
|
Matrix.det_fin_two_of
theorem Matrix.det_fin_two_of :
∀ {R : Type v} [inst : CommRing R] (a b c d : R), (Matrix.of ![![a, b], ![c, d]]).det = a * d - b * c
This theorem states that for any commutative ring `R`, the determinant of a 2x2 matrix with elements `a`, `b`, `c`, and `d` is equal to `a*d - b*c`. In mathematical terms, if we have a matrix
```
| a b |
| c d |
```
its determinant is computed as `a*d - b*c`. This is a specific case of the general determinant calculation for square matrices, and it aligns with the Leibniz formula for the determinant of a matrix.
More concisely: The determinant of a 2x2 commutative ring matrix [a b; c d] equals a*d - b*c.
|
Matrix.det_transpose
theorem Matrix.det_transpose :
∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (M : Matrix n n R),
M.transpose.det = M.det
This theorem states that the determinant of a transposed matrix is equal to the determinant of the original matrix. In other words, for any square matrix `M` with elements from a commutative ring `R`, and whose rows and columns are indexed by a finitely enumerable type `n` with a decidable equality, the determinant of the transpose of `M` is the same as the determinant of `M` itself. This property is important in linear algebra, where matrix transposition is a common operation.
More concisely: The determinant of a square matrix and its transpose are equal.
|
Matrix.det_eq_of_forall_row_eq_smul_add_pred
theorem Matrix.det_eq_of_forall_row_eq_smul_add_pred :
∀ {R : Type v} [inst : CommRing R] {n : ℕ} {A B : Matrix (Fin (n + 1)) (Fin (n + 1)) R} (c : Fin n → R),
(∀ (j : Fin (n + 1)), A 0 j = B 0 j) →
(∀ (i : Fin n) (j : Fin (n + 1)), A i.succ j = B i.succ j + c i * A i.castSucc j) → A.det = B.det
This theorem, titled `Matrix.det_eq_of_forall_row_eq_smul_add_pred`, states that for any type `R` that is a commutative ring and for any natural number `n`, given two `n+1` by `n+1` matrices `A` and `B` with entries in `R` and a function `c` from the set of `n`-element finite enumerations to `R`, if the first row of `A` and `B` are identical, and for all rows after the first in `A` and `B`, the entries in a row in `A` are equal to the corresponding entries in `B` plus some multiple (given by function `c`) of the entries in the previous row in `A`, then the determinants of `A` and `B` are equal. This theorem essentially confirms the invariance of determinant under the operation of adding multiples of previous rows to the next row.
More concisely: Given two `n+1` by `n+1` matrices `A` and `B` over a commutative ring `R`, if the first rows are equal and each subsequent row of `A` is the corresponding row of `B` with the previous row added and scaled by some constant from `R`, then the determinants of `A` and `B` are equal.
|
Matrix.det_apply'
theorem Matrix.det_apply' :
∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (M : Matrix n n R),
M.det = Finset.univ.sum fun σ => ↑↑(Equiv.Perm.sign σ) * Finset.univ.prod fun i => M (σ i) i
The theorem `Matrix.det_apply'` states that for any given square matrix `M` with entries in a commutative ring `R`, the determinant of `M` can be computed using the Leibniz formula. In this formula, `Finset.univ` is the set of all permutations on the index set `n`, and for each permutation `σ`, we take the product of `M (σ i) i` as `i` varies over the index set. We then multiply this product by the sign of the permutation `σ`, which is `1` for even permutations and `-1` for odd ones. Finally, we sum up these products over all permutations `σ`. This provides a combinatorial way to compute the determinant of a matrix.
More concisely: The determinant of a square matrix over a commutative ring can be calculated using the Leibniz formula, which involves summing the product of each entry in the matrix at row i and column σ(i), multiplied by the sign of the corresponding permutation σ, over all permutations of the index set.
|
Matrix.det_mul_column
theorem Matrix.det_mul_column :
∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (v : n → R)
(A : Matrix n n R), (Matrix.of fun i j => v i * A i j).det = (Finset.univ.prod fun i => v i) * A.det
The theorem `Matrix.det_mul_column` states that for a given type `n` (with decidable equality and which is a finite type), a commutative ring `R`, a function `v` from `n` to `R`, and a square matrix `A` with entries in `R` indexed by `n`, multiplying each column of `A` by the corresponding value in `v` results in the determinant of the new matrix being equal to the product of all values of `v` (over all `n`) times the determinant of the original matrix `A`. In terms of linear algebra, this means that scaling the columns of a matrix by a set of scalars results in the determinant being scaled by the product of those scalars.
More concisely: For a finite type `n`, commutative ring `R`, square matrix `A` of size `n x n` over `R`, and function `v : n → R`, the determinant of the matrix obtained by multiplying each column of `A` by the corresponding value in `v` is equal to the product of all values in `v` multiplied by the determinant of `A`.
|
Matrix.det_eq_elem_of_subsingleton
theorem Matrix.det_eq_elem_of_subsingleton :
∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R]
[inst_3 : Subsingleton n] (A : Matrix n n R) (k : n), A.det = A k k
This theorem states that for any type `n` with decidable equality and of finite type, and any commutative ring `R`, if `n` is a subsingleton (i.e., has at most one element), then the determinant of any matrix `A` with entries in `R` and with both row and column indices in `n`, is equal to the entry of `A` at position `(k,k)` for any `k` in `n`. In other words, if our matrix has a single element (as `n` is a subsingleton), then the determinant of the matrix is just that single element.
More concisely: For any commutative ring R and finite type n with decidable equality that is a subsingleton, the determinant of any matrix A over R with both row and column indices in n is equal to the entry of A at position (k,k) for any k in n.
|
Matrix.det_diagonal
theorem Matrix.det_diagonal :
∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {d : n → R},
(Matrix.diagonal d).det = Finset.univ.prod fun i => d i
The theorem `Matrix.det_diagonal` states that for any type `n` with decidable equality and finiteness, and any commutative ring `R`, given a function `d : n → R`, the determinant of a diagonal matrix created from `d` is equal to the product of all elements outputted by `d` when applied to each element of the universal finite set of `n`. In simpler terms, it's saying that the determinant of a diagonal matrix is the product of its diagonal elements.
More concisely: For any commutative ring R and type n with decidable equality and finiteness, the determinant of a diagonal matrix with diagonal entries d : n → R equals the product of the images of d applied to all elements of the universal finite set of n.
|
Matrix.det_fin_zero
theorem Matrix.det_fin_zero : ∀ {R : Type v} [inst : CommRing R] {A : Matrix (Fin 0) (Fin 0) R}, A.det = 1
This theorem is stating that for any commutative ring 'R', the determinant of a 0x0 matrix with entries in 'R' is always equal to 1. Note that 'Fin 0' is essentially representing a finite set with zero elements and 'Matrix (Fin 0) (Fin 0) R' is a matrix with zero rows and zero columns, or a 0x0 matrix. The 'det' function is used to calculate the determinant of a matrix. It means that the determinant of an empty matrix is defined to be the multiplicative identity in the ring, which is 1.
More concisely: The determinant of a 0x0 matrix over any commutative ring is equal to 1.
|
Matrix.det_isEmpty
theorem Matrix.det_isEmpty :
∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] [inst_3 : IsEmpty n]
{A : Matrix n n R}, A.det = 1
This theorem, `Matrix.det_isEmpty`, states that for any type `n` with decidable equality, which is a finite type, and assuming `n` is empty, if `R` is a type forming a commutative ring, then the determinant of any matrix `A`, which is a square matrix with entries in `R` and dimensions defined by `n`, is always equal to `1`.
More concisely: For any finite type `n` with decidable equality and any commutative ring `R`, if the square matrix `A` of dimension `n` over `R` is empty, then its determinant is equal to 1.
|
Matrix.det_fromBlocks_zero₁₂
theorem Matrix.det_fromBlocks_zero₁₂ :
∀ {m : Type u_1} {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
[inst_3 : Fintype m] {R : Type v} [inst_4 : CommRing R] (A : Matrix m m R) (C : Matrix n m R) (D : Matrix n n R),
(A.fromBlocks 0 C D).det = A.det * D.det
The theorem `Matrix.det_fromBlocks_zero₁₂` states that for any arbitrary types `m` and `n`, given that `n` and `m` have decidable equality and are finite, and any commutative ring `R`, the determinant of a 2x2 block matrix (constructed by the `fromBlocks` function) with its upper-right block being zero is equal to the product of the determinants of the diagonal blocks. The diagonal blocks here are represented by the matrices `A` and `D`. This particular case is a precursor to a more generalized theorem that applies to any number of blocks, as stated in `Matrix.det_of_lower_triangular`.
More concisely: For any finite and commutative ring R, the determinant of a 2x2 block matrix with a zero upper-right block is equal to the product of the determinants of its diagonal blocks.
|
Matrix.det_fin_two
theorem Matrix.det_fin_two :
∀ {R : Type v} [inst : CommRing R] (A : Matrix (Fin 2) (Fin 2) R), A.det = A 0 0 * A 1 1 - A 0 1 * A 1 0
This theorem, named `Matrix.det_fin_two`, states that for any 2x2 matrix `A` with elements in a commutative ring `R`, the determinant of `A` is calculated as the product of the elements at the first row and the second column (i.e., `A 0 0` and `A 1 1`) minus the product of the elements at the first column and the second row (i.e., `A 0 1` and `A 1 0`). In other words, this is the standard formula for the determinant of a 2x2 matrix.
More concisely: The determinant of a 2x2 matrix over a commutative ring is equal to the product of its first row's first and second elements, minus the product of its first column's first and second elements.
|
Matrix.det_eq_of_forall_col_eq_smul_add_pred
theorem Matrix.det_eq_of_forall_col_eq_smul_add_pred :
∀ {R : Type v} [inst : CommRing R] {n : ℕ} {A B : Matrix (Fin (n + 1)) (Fin (n + 1)) R} (c : Fin n → R),
(∀ (i : Fin (n + 1)), A i 0 = B i 0) →
(∀ (i : Fin (n + 1)) (j : Fin n), A i j.succ = B i j.succ + c j * A i j.castSucc) → A.det = B.det
This theorem states that, for any two square matrices A and B of order (n+1) with elements in a commutative ring R and any function c that assigns an element of R to each natural number from 0 to n-1 (exclusive), if the first column of A and B are the same and for all subsequent columns, the ith entry of the jth column of A is equal to the ith entry of the jth column of B plus the jth value of c times the ith entry of the (j-1)th column of A, then the determinants of A and B are equal. This means that if you add multiples of previous columns to the next columns in a matrix, the determinant of the matrix doesn't change.
More concisely: If two square matrices of order n+1 over a commutative ring, with the same first column and such that the ith entry of the jth column of the first matrix is equal to the ith entry of the jth column of the second, plus the jth value of a function c times the ith entry of the (j-1)th column of the first, have equal determinants.
|
Matrix.det_fromBlocks_zero₂₁
theorem Matrix.det_fromBlocks_zero₂₁ :
∀ {m : Type u_1} {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
[inst_3 : Fintype m] {R : Type v} [inst_4 : CommRing R] (A : Matrix m m R) (B : Matrix m n R) (D : Matrix n n R),
(A.fromBlocks B 0 D).det = A.det * D.det
This theorem states that the determinant of a 2x2 block matrix, with the lower-left block being zero, equals the product of the determinants of the diagonal blocks. This is valid for any types `m` and `n` that have decidable equality and are finite, and for any commutative ring `R`. The matrix `A` is a square matrix indexed by `m`, `B` is a matrix indexed by `m` and `n`, and `D` is a square matrix indexed by `n`.
More concisely: If `A` is a square `m x m` matrix, `B` is an `m x n` matrix with a zero lower-left block, and `D` is an `n x n` matrix, then the determinant of the block matrix `[A | B]` equals the product of the determinant of `A` and the determinant of `D`, assuming `m` and `n` are finite types with decidable equality and `R` is a commutative ring.
|
Matrix.det_one
theorem Matrix.det_one :
∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R], Matrix.det 1 = 1
This theorem, `Matrix.det_one`, states that for any type `n` with decidable equality and finite instances, and any commutative ring `R`, the determinant of the identity matrix is 1. Here, `Matrix.det 1` represents the determinant of the identity matrix, and the theorem asserts that this determinant equals 1, which is a well-known property of identity matrices in linear algebra.
More concisely: For any commutative ring R and finite type n with decidable equality, the determinant of the identity matrix of size n over R is equal to 1.
|
Matrix.det_smul
theorem Matrix.det_smul :
∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (A : Matrix n n R)
(c : R), (c • A).det = c ^ Fintype.card n * A.det
The `Matrix.det_smul` theorem states that for any type `n` with decidable equality and finite number of elements, and any commutative ring `R`, if `A` is a matrix of size `n` by `n` with entries in `R` and `c` is an element of `R`, then the determinant of the matrix obtained by scaling `A` by `c` is equal to `c` raised to the power of the number of elements in `n` times the determinant of `A`. In mathematical terms, for a square matrix `A` and scalar `c`, it asserts that `det(cA) = c^n * det(A)`, where `n` is the dimension of the matrix.
More concisely: For any square matrix `A` of dimension `n` over a commutative ring `R` with decidable equality and finite number of elements, and any scalar `c` in `R`, the determinant of the matrix `cA` is equal to `c^n` times the determinant of `A`.
|
Matrix.det_reindex_self
theorem Matrix.det_reindex_self :
∀ {m : Type u_1} {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
[inst_3 : Fintype m] {R : Type v} [inst_4 : CommRing R] (e : m ≃ n) (A : Matrix m m R),
((Matrix.reindex e e) A).det = A.det
The theorem `Matrix.det_reindex_self` states that if you have a matrix `A` whose rows and columns are indexed by the same type `m`, and there's an equivalence `e` between `m` and another type `n`, then reindexing both rows and columns of `A` along this equivalence `e` will preserve the determinant of the matrix. That is, the determinant of the reindexed matrix is equal to the determinant of the original matrix `A`. This is true for any ring `R` and for any types `m` and `n` that have decidable equality and are finite. In other words, rearranging the rows and columns of a matrix in a consistent manner does not change the determinant of the matrix. The proof of this theorem is not shown here.
More concisely: If `A` is a matrix over a ring `R` with finite, decidably equalized indices `m` and `n`, then the determinant of `A` is equal to the determinant of `A` reindexed along an equivalence between `m` and `n`.
|
Matrix.det_apply
theorem Matrix.det_apply :
∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (M : Matrix n n R),
M.det = Finset.univ.sum fun σ => Equiv.Perm.sign σ • Finset.univ.prod fun i => M (σ i) i
The theorem `Matrix.det_apply` states that for any square matrix `M` with entries in a commutative ring `R`, and whose rows and columns are indexed by a type `n` that has decidable equality and is finite, the determinant of `M` is equal to the sum, over all permutations `σ`, of the product of the sign of `σ` and the product, over all indices `i`, of the `i`-th row and `σ(i)`-th column entry of `M`. It essentially expresses the determinant of a matrix in terms of the Leibniz formula.
More concisely: The determinant of a square matrix over a commutative ring with decidable equality and finite index type is equal to the sum, over all permutations, of the sign of the permutation times the product of the corresponding row-column entries.
|
Matrix.det_mul_right_comm
theorem Matrix.det_mul_right_comm :
∀ {m : Type u_1} [inst : DecidableEq m] [inst_1 : Fintype m] {R : Type v} [inst_2 : CommRing R]
(M N P : Matrix m m R), (M * N * P).det = (M * P * N).det
This theorem, `Matrix.det_mul_right_comm`, states that for any type `m` which has decidable equality and is a finite type, and any commutative ring `R`, the determinant of the product of three square matrices `M`, `N`, `P`, all of which have entries in `R` and are indexed by `m`, is commutative with respect to right multiplication. In other words, the determinant of the product `M * N * P` is equal to the determinant of the product `M * P * N`.
More concisely: For any commutative ring R and finite type m with decidable equality, the determinant of the product of three square matrices M, N, and P over R with dimensions m x m is commutative with respect to right multiplication: det(M * N * P) = det(M * P * N).
|
Matrix.det_mul_comm
theorem Matrix.det_mul_comm :
∀ {m : Type u_1} [inst : DecidableEq m] [inst_1 : Fintype m] {R : Type v} [inst_2 : CommRing R]
(M N : Matrix m m R), (M * N).det = (N * M).det
This theorem states that for any square matrices `M` and `N` over a commutative ring `R`, the determinant of the product of `M` and `N` is equal to the determinant of the product of `N` and `M`. In other words, the order of multiplication of matrices does not change the determinant. This property holds for any type `m` indexing the rows and columns of the matrices, as long as there is a decidable equality on `m` and `m` is finite.
More concisely: For any commutative ring R and finite, indexed square matrices M and N over R, the determinant of the product M * N is equal to the determinant of N * M.
|
RingHom.map_det
theorem RingHom.map_det :
∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {S : Type w}
[inst_3 : CommRing S] (f : R →+* S) (M : Matrix n n R), f M.det = (f.mapMatrix M).det
The theorem `RingHom.map_det` states that for any types `n`, `R`, and `S` where `n` has decidable equality and is a finite type, `R` and `S` are commutative rings, any ring homomorphism `f` from `R` to `S`, and any matrix `M` with elements in `R` and indices in `n`, the determinant of the matrix `M` after applying the ring homomorphism `f` to each of its elements is equal to the result of applying `f` to the determinant of `M`. In other words, the mapping of the determinant of a matrix under a ring homomorphism is equal to the determinant of the matrix obtained by mapping each element of the original matrix under the same ring homomorphism. This is expressed mathematically as `f(det(M)) = det(f(M))` where `f` is the ring homomorphism and `M` is the matrix.
More concisely: The determinant of a matrix under a ring homomorphism is equal to the ring homomorphism's application to the determinant of the original matrix. In other words, `f(det(M)) = det(f(M))` for any commutative rings `R` and `S`, finite type `n` with decidable equality, and ring homomorphism `f` from `R` to `S`.
|
Matrix.det_succ_row
theorem Matrix.det_succ_row :
∀ {R : Type v} [inst : CommRing R] {n : ℕ} (A : Matrix (Fin n.succ) (Fin n.succ) R) (i : Fin n.succ),
A.det = Finset.univ.sum fun j => (-1) ^ (↑i + ↑j) * A i j * (A.submatrix i.succAbove j.succAbove).det
The theorem `Matrix.det_succ_row` states that for any commutative ring `R`, and for any natural number `n`, if `A` is an `(n+1) x (n+1)` matrix with entries from `R`, and `i` is a row index in `A`, then the determinant of `A` can be computed by summing over all columns `j` in `A`, the product of `(-1) ^ (i + j)`, the element at row `i` and column `j` in `A`, and the determinant of the submatrix of `A` that results from removing the `i`-th row and `j`-th column. This is known as the Laplacian expansion of a determinant along a row.
More concisely: For any commutative ring R and an (n+1)x(n+1) matrix A over R, the determinant of A can be computed as the sum over all i and j, where i is a row index and j is a column index, of (-1) ^ (i+j) * (the entry of A in row i and column j) * determinant of the submatrix of A obtained by removing row i and column j.
|
Matrix.det_unique
theorem Matrix.det_unique :
∀ {R : Type v} [inst : CommRing R] {n : Type u_3} [inst_1 : Unique n] [inst_2 : DecidableEq n] [inst_3 : Fintype n]
(A : Matrix n n R), A.det = A default default
The theorem `Matrix.det_unique` states that if a type `n` has only one element (expressed by the `Unique n` condition), then the determinant of any `n` by `n` matrix (whose entries are elements of a commutative ring `R`) is just that single element of `n`. Specifically, for such a matrix `A`, `Matrix.det A = A default default`, where `default` is the unique element of `n`. Note that while the `Unique` condition implies `DecidableEq` and `Fintype`, these instances may not be syntactically identical, so they need to be provided explicitly.
More concisely: If a square matrix over a commutative ring has determinant and its entries form a type with only one element, then the determinant equals that unique element.
|
Matrix.det_mul
theorem Matrix.det_mul :
∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R]
(M N : Matrix n n R), (M * N).det = M.det * N.det
This theorem states that, for any type `n` with decidable equality and finite number of elements, and any commutative ring `R`, the determinant of the product of two matrices `M` and `N` (whose entries are in `R` and both are indexed by `n`) is equal to the product of the determinants of `M` and `N`. In other words, it formalizes the well-known property from linear algebra: if `M` and `N` are square matrices, then `det(M * N) = det(M) * det(N)`.
More concisely: For any commutative ring R and finite type n with decidable equality, the determinant of the product of two n x n matrices over R is equal to the product of their determinants.
|
Matrix.det_permute
theorem Matrix.det_permute :
∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (σ : Equiv.Perm n)
(M : Matrix n n R), (M.submatrix (⇑σ) id).det = ↑↑(Equiv.Perm.sign σ) * M.det
The theorem `Matrix.det_permute` states that for any finite type `n` with decidable equality, a commutative ring `R`, a permutation `σ` of `n`, and a square matrix `M` with entries in `R`, the determinant of the submatrix obtained by permuting the columns of `M` according to `σ` is equal to the sign of `σ` times the determinant of `M`. In other words, permuting the columns of a matrix changes the sign of its determinant. The sign of the permutation is `1` for even permutations and `-1` for odd permutations.
More concisely: The determinant of a square matrix with entries in a commutative ring is changed by a sign equal to the parity of the permutation when permuting its columns.
|
Matrix.det_permutation
theorem Matrix.det_permutation :
∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (σ : Equiv.Perm n),
(Equiv.toPEquiv σ).toMatrix.det = ↑↑(Equiv.Perm.sign σ)
This theorem states that for any permutation σ (represented as a bijection from a set `n` to itself), and in the context where `n` has decidable equality and is a finite type, and `R` is a commutative ring, the determinant of the permutation matrix corresponding to σ is equal to the sign of σ. A permutation matrix is a square binary matrix with exactly one entry of 1 in each row and each column and 0s elsewhere. The sign of a permutation is `1` for even permutations and `-1` for odd ones.
More concisely: For any finite, decidably equal set `n` and commutative ring `R`, the determinant of the permutation matrix corresponding to a bijection (permutation) σ from `n` to itself equals the sign of σ.
|