Matrix.derivative_det_one_add_X_smul
theorem Matrix.derivative_det_one_add_X_smul :
∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R),
Polynomial.eval 0 (Polynomial.derivative (1 + Polynomial.X • M.map ⇑Polynomial.C).det) = M.trace
This theorem states that for a commutative ring `R` and a finite type `n`, given a square matrix `M` with entries from `R` and indices from `n`, the derivative of the determinant of the matrix `(1 + M X)`, evaluated at `0`, is equivalent to the trace of the matrix `M`. Here, `X` represents the polynomial variable, and `Polynomial.C` is a function that maps a ring element to a constant polynomial of that element. The derivative and the evaluation of the polynomial are computed following the usual rules of calculus and polynomial evaluation.
More concisely: For a commutative ring `R` and a finite type `n`, the derivative of the determinant of the matrix `(I + M)` evaluated at `0`, where `I` is the identity matrix and `M` is a square matrix with entries from `R` and indices from `n`, equals the trace of `M`.
|
Matrix.det_one_add_smul
theorem Matrix.det_one_add_smul :
∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (r : R)
(M : Matrix n n R),
(1 + r • M).det =
1 + M.trace * r + Polynomial.eval r (1 + Polynomial.X • M.map ⇑Polynomial.C).det.divX.divX * r ^ 2
This theorem, "Matrix.det_one_add_smul", states that for any commutative ring `R`, any type `n` with decidable equality and finite instances, any scalar `r` from `R`, and any square matrix `M` with entries in `R`, the determinant of the matrix `(1 + r • M)` equals to `1` plus the product of the trace of `M` and `r`, plus the evaluation at `r` of the determinant of the matrix `(1 + Polynomial.X • M.map ⇑Polynomial.C)` divided twice by `X`, all multiplied by `r` squared. This represents the first two terms of the Taylor expansion of `det (1 + r • M)` at `r = 0`.
More concisely: For any commutative ring `R`, matrix `M` of size `n` over `R` with decidable equality and finite instances, scalar `r` in `R`, the determinant of the matrix `(1 + r • M)` equals `1 + r * (trace M + r * (det M / (2 * X) ^ 2))`, where `X` is a variable representing an indeterminate.
|
Matrix.pow_eq_aeval_mod_charpoly
theorem Matrix.pow_eq_aeval_mod_charpoly :
∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R)
(k : ℕ), M ^ k = (Polynomial.aeval M) ((Polynomial.X ^ k).modByMonic M.charpoly)
This theorem states that for any matrix 'M' with entries from a commutative ring 'R' and indices from a decidable equality type 'n' that is also a finite type, any power 'k' of this matrix can be computed as the evaluation of a polynomial applied to 'M'. The polynomial in question is obtained by taking the 'k'-th power of the polynomial variable 'X' and then reducing it modulo the characteristic polynomial of the matrix 'M'. This result essentially connects the algebra of matrices with the algebra of polynomials over a ring. Note that a future extension of this theorem is planned to accommodate negative powers of the matrix, using the concept of 'zpow'.
More concisely: For any square matrix M with entries from a commutative ring and finite decidable equality type indices, any power of M can be expressed as the reduction of X^k modulo the characteristic polynomial of M, where X is a polynomial variable.
|
Matrix.aeval_eq_aeval_mod_charpoly
theorem Matrix.aeval_eq_aeval_mod_charpoly :
∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R)
(p : Polynomial R), (Polynomial.aeval M) p = (Polynomial.aeval M) (p.modByMonic M.charpoly)
The theorem `Matrix.aeval_eq_aeval_mod_charpoly` states that for any ring `R` with commutative operations, any matrix `M` (with decidable equality and finite type for its indices) over `R`, and any polynomial `p` with coefficients in `R`, the result of evaluating the polynomial `p` at the matrix `M` is equal to the result of evaluating the polynomial, which is obtained by taking modulo of `p` by the characteristic polynomial of `M` and assumed to be monic, at the matrix `M`. This theorem asserts that the polynomial `p` is equivalent to a polynomial of degree less than the dimension of the matrix when evaluated at that matrix.
More concisely: For any commutative ring R, matrix M over R with decidable equality and finite type indices, and monic polynomial p with coefficients in R, the evaluation of p at M is equal to the remainder of p divided by the characteristic polynomial of M when both are evaluated at M.
|
Matrix.trace_eq_neg_charpoly_coeff
theorem Matrix.trace_eq_neg_charpoly_coeff :
∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] [inst_3 : Nonempty n]
(M : Matrix n n R), M.trace = -M.charpoly.coeff (Fintype.card n - 1)
The theorem `Matrix.trace_eq_neg_charpoly_coeff` states that for any commutative ring `R` and any type `n` with decidable equality, finite cardinality, and at least one element, the trace of an `n x n` matrix `M` with entries in `R` is equal to the negative of the coefficient of the term `X^(n-1)` in the characteristic polynomial of `M`. The characteristic polynomial of `M` is defined as the determinant of `(tI - M)`, where `I` is the identity matrix and `t` is a variable. The trace of a matrix is the sum of its diagonal entries.
More concisely: For any commutative ring R and finite type n with at least one element, the trace of an n x n matrix M over R equals the negative of the coefficient of X^(n-1) in the determinant of (tI - M), where t is a variable and I is the identity matrix.
|
Matrix.charpoly_degree_eq_dim
theorem Matrix.charpoly_degree_eq_dim :
∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n]
[inst_3 : Nontrivial R] (M : Matrix n n R), M.charpoly.degree = ↑(Fintype.card n)
This theorem states that for any commutative ring `R`, any type `n` which has decidable equality and is finite, and any nontrivial element of `R`, the degree of the characteristic polynomial of a `n` by `n` matrix `M` with entries in `R` is equal to the cardinality (number of elements) of the type `n` (which represents the dimension of the matrix `M`). In mathematical terms, this theorem conveys that the degree of the characteristic polynomial of a square matrix is equal to the dimension of the matrix.
More concisely: For any commutative ring with decidable equality and finite type `n`, the degree of the characteristic polynomial of a `n` by `n` matrix over that ring equals the cardinality of `n`.
|
Matrix.charpoly_natDegree_eq_dim
theorem Matrix.charpoly_natDegree_eq_dim :
∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n]
[inst_3 : Nontrivial R] (M : Matrix n n R), M.charpoly.natDegree = Fintype.card n
The theorem `Matrix.charpoly_natDegree_eq_dim` states that for any commutative ring `R` and any finite type `n` that has decidable equality, given a nontrivial matrix `M` with entries in `R` and both its rows and columns indexed by `n`, the natural degree of the characteristic polynomial of `M` is equal to the number of elements in `n`. This can be understood as the degree of the characteristic polynomial of a matrix being equal to the dimension of the matrix in the field of the matrix entries.
More concisely: For any commutative ring with decidable equality `R` and a finite type `n`, the natural degree of the characteristic polynomial of a nontrivial `n x n` matrix over `R` equals the number of elements in `n`.
|
Matrix.charpoly_monic
theorem Matrix.charpoly_monic :
∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R),
M.charpoly.Monic
The theorem `Matrix.charpoly_monic` states that for any type `R` with a commutative ring structure, for any finite type `n` with decidable equality, and for any matrix `M` of size `n x n` with entries in `R`, the characteristic polynomial of `M` is monic. In other words, the leading coefficient of the characteristic polynomial of any such matrix `M` is 1.
More concisely: The characteristic polynomial of any square matrix over a commutative ring with decidable equality has a leading coefficient of 1.
|