Matrix.adjugate_mul_distrib
theorem Matrix.adjugate_mul_distrib :
∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A B : Matrix n n α),
(A * B).adjugate = B.adjugate * A.adjugate
This theorem, `Matrix.adjugate_mul_distrib`, states that for any two matrices `A` and `B` of the same dimensions, where the entries of the matrices are elements of a commutative ring, and the indices of the matrices have decidable equality and finite type, the adjugate of the product of `A` and `B` is equal to the product of the adjugate of `B` and the adjugate of `A`. This is a property of the adjugate operation related to matrix multiplication, essentially saying that adjugate operation distributes over matrix multiplication, but in a reversed order. This result is a consequence of the trace Cayley-Hamilton theorem, as referred to in the work by Darij Grinberg.
More concisely: For matrices A and B of equal dimensions over a commutative ring with decidable entries and finite type indices, the adjugate of their product is equal to the product of their adjugates.
|
Matrix.sum_cramer_apply
theorem Matrix.sum_cramer_apply :
∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A : Matrix n n α)
{β : Type u_1} (s : Finset β) (f : n → β → α) (i : n),
(s.sum fun x => A.cramer (fun j => f j x) i) = A.cramer (fun j => s.sum fun x => f j x) i
The theorem `Matrix.sum_cramer_apply` states that for any type `n` with a decidable equality and finite number of elements, any type `α` that forms a commutative ring, any matrix `A` with entries in `α` and indices in `n`, any type `β`, any finite set `s` of type `β`, any function `f` from `n` and `β` to `α`, and any index `i` of type `n`, the sum across `s` of the Cramer's Rule applied to the function `f` with respect to `i` and the matrix `A` is equal to the Cramer's Rule applied to the sum across `s` of the function `f` with respect to `i` and the matrix `A`. In other words, it states the linearity of the Cramer's Rule in the context of summation, allowing the Cramer's Rule to be taken out of the sum.
More concisely: For any commutative ring `α` with decidable equality and finite number of elements, any finite set `s`, and any function `f` from the finite index set and `s` to `α`, the sum of Cramer's Rule applications to `f` and a square matrix `A` with respect to a fixed index is equal to the Cramer's Rule application to the sum of `f` and the matrix `A`.
|
Matrix.sum_cramer
theorem Matrix.sum_cramer :
∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A : Matrix n n α)
{β : Type u_1} (s : Finset β) (f : β → n → α), (s.sum fun x => A.cramer (f x)) = A.cramer (s.sum fun x => f x)
The theorem `Matrix.sum_cramer` states that for any matrix `A` of type `Matrix n n α`, where `n` is a type with decidable equality, `α` is a commutative ring, and `A` is square (i.e., its row and column indices are of the same type `n`), and for any finite set `s` of type `β` and a function `f` from `β` to `n` producing entries of type `α`, the sum of applying the `cramer` function to `A` with the output of `f` for each element of `s` is equal to the result of applying the `cramer` function to `A` with the sum of the outputs of `f` for all elements of `s`. In essence, this theorem verifies that the `cramer` function, which typically determines the solution to a system of linear equations, is linear over the summation for a set of values.
More concisely: For any square matrix A of type n x n over a commutative ring α with decidable equality, and any function f from a finite set to the index type n producing matrix entries, the sum of the Cramer's rule determinants using f(s) for all s in the set equals the Cramer's rule determinant using the sum of f(s) for all s in the set.
|
Matrix.adjugate_adjugate
theorem Matrix.adjugate_adjugate :
∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A : Matrix n n α),
Fintype.card n ≠ 1 → A.adjugate.adjugate = A.det ^ (Fintype.card n - 2) • A
This theorem states that for any type `n` and type `α`, assuming that `n` has decidable equality and is a finite type, and `α` is a commutative ring, given a square matrix `A` of type `α` with `n` rows and `n` columns, the adjugate of the adjugate of `A` equals the determinant of `A` raised to the power of "the number of elements in `n` minus 2" scaled by `A`. However, this theorem is not valid when the number of elements in `n` equals 1 because `1 - 2` equals `-1` and not `0`.
More concisely: For a finite commutative ring type `α` with decidable equality and a square matrix `A` of size `n × n` over `α`, the adjugate of the adjugate of `A` equals the determinant of `A` raised to the power of `(n-2)` multiplied by `A`. (This statement holds only when `n > 1`.)
|
Matrix.adjugate_adjugate'
theorem Matrix.adjugate_adjugate' :
∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A : Matrix n n α)
[inst_3 : Nontrivial n], A.adjugate.adjugate = A.det ^ (Fintype.card n - 2) • A
This theorem, termed `Matrix.adjugate_adjugate'`, declares that for any square matrix `A` with entries in a commutative ring `α`, whose rows and columns are indexed by a finite and decidable equivalence type `n`, given that `n` is nontrivial (it has at least two distinct elements), the adjugate of the adjugate of `A` is equal to `A` scaled by the determinant of `A` raised to the power of the cardinality (number of elements) of `n` minus two. In mathematical notation, this is equivalent to stating that for a matrix $A$, $(adj(adj(A)) = det(A)^{card(n) - 2} * A$. The `adjugate` of a matrix, often denoted `adj(A)`, is the transpose of the cofactor matrix of `A`, and the determinant, `det(A)`, is a special value calculated from the elements of `A`.
More concisely: For any square matrix $A$ over a commutative ring with finite and decidable indices $n$, with $n$ nontrivial, adj(adj(A)) = det(A)^{(|n|-2)} * A.
|
Matrix.cramer_apply
theorem Matrix.cramer_apply :
∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A : Matrix n n α)
(b : n → α) (i : n), A.cramer b i = (A.updateColumn i b).det
This theorem states that for any square matrix `A` of type `Matrix n n α` with entries in a commutative ring `α`, and any vector `b` of type `n → α`, the `i`-th component of the vector obtained by applying Cramer's rule to `A` and `b`, `(Matrix.cramer A) b i`, is equal to the determinant of the matrix obtained by replacing the `i`-th column of `A` with `b`, `Matrix.det (Matrix.updateColumn A i b)`. This is a formal statement of a standard result in linear algebra regarding the computation of solutions to a system of linear equations using Cramer's rule.
More concisely: For any square matrix `A` and vector `b`, the `i`-th component of the vector obtained by applying Cramer's rule to `A` and `b` equals the determinant of the matrix obtained by replacing the `i`-th column of `A` with `b`.
|
Matrix.mul_adjugate
theorem Matrix.mul_adjugate :
∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A : Matrix n n α),
A * A.adjugate = A.det • 1
This theorem states that for any square matrix `A` (with elements in a commutative ring `α` and size determined by type `n` which has decidable equality and is finite), the product of `A` and the adjugate of `A` is equal to the determinant of `A` scaled by the identity matrix. The adjugate of a matrix is the transpose of the cofactor matrix, and the identity matrix is a square matrix with ones on the diagonal and zeros elsewhere. The `•` operator in Lean 4 denotes scalar multiplication, where a number multiplies every element of the matrix.
More concisely: For any square matrix `A` of size `n` over a commutative ring with decidable equality and finite elements, `A * adj_mat A = det A • id`, where `adj_mat A` is the adjugate of `A`, `det A` is the determinant of `A`, and `id` is the identity matrix.
|
Matrix.adjugate_transpose
theorem Matrix.adjugate_transpose :
∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A : Matrix n n α),
A.adjugate.transpose = A.transpose.adjugate
This theorem states that for any square matrix `A` with elements from a commutative ring `α`, the transpose of the adjugate of `A` equals the adjugate of the transpose of `A`. The theorem assumes the size `n` of the matrix `A` is a finite type and has decidable equality. In mathematical terms, if `A` is a square matrix, then `(adj(A))^T = adj(A^T)`, where `adj` denotes the adjugate of a matrix, `T` denotes the transpose of the matrix, and `^` denotes exponentiation.
More concisely: For any square matrix A over a commutative ring of finite type with decidable equality, the transpose of the adjugate of A is equal to the adjugate of the transpose of A. (In mathematical notation: adj(A)^T = adj(A^T))
|
Matrix.mulVec_cramer
theorem Matrix.mulVec_cramer :
∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A : Matrix n n α)
(b : n → α), A.mulVec (A.cramer b) = A.det • b
This theorem is a stronger version of Cramer's rule in linear algebra. Cramer's rule is a method used to solve systems of linear equations. The theorem states that for any types `n` and `α`, where `n` has a decidable equality and is a finite type, and `α` is a commutative ring, given a square matrix `A` (of type `α` and indexed by `n`) and a vector `b` (indexed by `n`), the result of multiplying the matrix `A` by the vector resulting from applying Cramer's rule on `A` and `b` is equal to the determinant of `A` scaled by the vector `b`. A key aspect of this version of the theorem is that it can solve some instances of the system of linear equations `A * x = b` even if the determinant of `A` is not a unit, provided the determinant of `A` divides `b`.
More concisely: For any finite type `n` with decidable equality and commutative ring `α`, if `A` is an `n × n` matrix over `α` and `b` is a vector of length `n` over `α`, then `det A * (Cramer's rule vector for A and b) = A * b` if `det A` divides `b`.
|
Matrix.cramer_eq_adjugate_mulVec
theorem Matrix.cramer_eq_adjugate_mulVec :
∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A : Matrix n n α)
(b : n → α), A.cramer b = A.adjugate.mulVec b
The theorem `Matrix.cramer_eq_adjugate_mulVec` states that for any type `n`, any type `α` which has decidable equality and is a commutative ring, and any matrix `A` of type `Matrix n n α` (i.e., a square matrix with entries in `α`), the result of applying the Cramer's Rule (represented by `A.cramer b`) to any vector `b` (represented by `n → α`) is equal to the result of multiplying the adjugate of `A` with the vector `b`. This theorem is based on the linear property of the map `b ↦ cramer A b`.
More concisely: For any square matrix A of size n over a commutative ring α with decidable equality, Cramer's Rule (A.cramer b) equals the product of the adjugate of A and vector b.
|
Matrix.adjugate_subsingleton
theorem Matrix.adjugate_subsingleton :
∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α]
[inst_3 : Subsingleton n] (A : Matrix n n α), A.adjugate = 1
This theorem states that for any type `n`, type `α`, any instance of decidable equality on `n`, any instance indicating `n` is finite, any instance of a commutative ring defined on `α`, and any instance proving `n` is a subsingleton (meaning it has at most one element), the adjugate of a matrix `A` of type `Matrix n n α` (which is a matrix with entries in `α`, whose rows and columns are indexed by `n`) is the identity matrix. In mathematical terms, if we have a matrix `A` derived from a commutative ring and `n` is a set with at most one element, then the adjugate of `A` is the identity matrix.
More concisely: For any finite, subsingleton type `n` and commutative ring `α`, the adjugate of a matrix `A` of size `n x n` over `α` is the identity matrix.
|
Matrix.adjugate_apply
theorem Matrix.adjugate_apply :
∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A : Matrix n n α)
(i j : n), A.adjugate i j = (A.updateRow j (Pi.single i 1)).det
This theorem, `Matrix.adjugate_apply`, states that for any square matrix `A` with elements of a commutative ring `α`, and for any pair of indices `(i, j)`, the `(i,j)`-th entry of the adjugate of `A` equals the determinant of the matrix obtained by updating the `j`-th row of `A` with the function supported at `i` with value `1` and `0` elsewhere. In other words, the adjugate of `A` at position `(i, j)` is computed by replacing the `j`-th row of `A` with a row that has `1` at the `i`-th position and `0`'s elsewhere, and calculating the determinant of the resulting matrix.
More concisely: The `(i, j)`-th entry of the adjugate of a square matrix `A` over a commutative ring is equal to the determinant of the matrix obtained by replacing the `j`-th row of `A` with the `i`-th row and setting all other entries in the replaced row to zero.
|
Matrix.adjugate_mul
theorem Matrix.adjugate_mul :
∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A : Matrix n n α),
A.adjugate * A = A.det • 1
The theorem `Matrix.adjugate_mul` states that for any square matrix `A` of type `α` where `α` is a commutative ring, the product of the adjugate of `A` and `A` itself is equal to the determinant of `A` times the identity matrix. This theorem holds for any matrix size `n`, where `n` is a finite type with decidable equality.
More concisely: The theorem asserts that that the product of the adjugate and a square matrix over a commutative ring equals the determinant of the matrix multiplied by the identity matrix.
|