Matrix.aeval_self_charpoly
theorem Matrix.aeval_self_charpoly :
∀ {R : Type u_1} [inst : CommRing R] {n : Type u_4} [inst_1 : DecidableEq n] [inst_2 : Fintype n]
(M : Matrix n n R), (Polynomial.aeval M) M.charpoly = 0
The Cayley-Hamilton theorem states that the characteristic polynomial of a matrix, when applied to the matrix itself, yields zero. This theorem holds for any commutative ring. In particular, for any commutative ring `R`, and for any matrix `M` with entries in `R` and indices from a decidable and finite type `n`, the algebra homomorphism generated by applying the polynomial `Matrix.charpoly M` to the matrix `M` results in zero. There is an equivalent statement about endomorphisms, `LinearMap.aeval_self_charpoly`.
More concisely: The characteristic polynomial of a matrix, when evaluated at the matrix itself, yields the zero matrix.
|
Matrix.charmatrix_apply_ne
theorem Matrix.charmatrix_apply_ne :
∀ {R : Type u_1} [inst : CommRing R] {n : Type u_4} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R)
(i j : n), i ≠ j → M.charmatrix i j = -Polynomial.C (M i j)
This theorem states that for any commutative ring `R`, any finite type `n` with decidable equality, and any matrix `M` with entries in `R` and indices in `n`, if the row index `i` is not equal to the column index `j`, then the entry of the characteristic matrix of `M` at `(i, j)` is equal to the negation of the entry of `M` at `(i, j)` under the constant polynomial map. In other words, for non-diagonal entries, the characteristic matrix contains the negation of the original matrix's entries, converted to constant polynomials.
More concisely: For any commutative ring `R`, finite type `n` with decidable equality, and matrix `M` over `R` with indices in `n`, the non-diagonal entries of the characteristic matrix of `M` are the negations of the constant polynomial evaluations of `M`'s entries.
|
Matrix.charmatrix_apply_eq
theorem Matrix.charmatrix_apply_eq :
∀ {R : Type u_1} [inst : CommRing R] {n : Type u_4} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R)
(i : n), M.charmatrix i i = Polynomial.X - Polynomial.C (M i i)
The theorem `Matrix.charmatrix_apply_eq` states that for any commutative ring `R`, any finite type `n` with decidable equality, and any square matrix `M` of type `n` with entries in `R` and any index `i` of type `n`, the `i`-`i` entry of the characteristic matrix of `M` is equal to the polynomial variable `X` minus the constant polynomial of the `i`-`i` entry of `M`. In mathematical terms, it says that the diagonal entry of the characteristic matrix of a square matrix is `X - M[i,i]`, where `X` is the polynomial variable and `M[i,i]` is the `i`-`i`th entry of the matrix `M`.
More concisely: The characteristic matrix of a square matrix over a commutative ring with decidable equality has the `i`-`th` diagonal entry equal to `X` minus the entry in the `i`-`th` row and column.
|