Matrix.mvPolynomialX_mapMatrix_aeval
theorem Matrix.mvPolynomialX_mapMatrix_aeval :
∀ {m : Type u_1} (R : Type u_3) {S : Type u_4} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : CommSemiring R]
[inst_3 : CommSemiring S] [inst_4 : Algebra R S] (A : Matrix m m S),
(MvPolynomial.aeval fun p => A p.1 p.2).mapMatrix (Matrix.mvPolynomialX m m R) = A
This theorem is a variant of `Matrix.mvPolynomialX_map_eval₂` and it states that for any finite type `m`, any commutative semirings `R` and `S`, any algebra structure on `R` and `S`, and any matrix `A` with entries in `S`, the algebra homomorphism (`MvPolynomial.aeval`) from multivariate polynomials over `m` to `S` generated by a map that takes a pair of indices and returns the corresponding entry in `A`, when applied to the matrix whose entries are multivariate polynomials in variables indexed by pairs from `m`, results in the original matrix `A`. In other words, when we replace each variable in the matrix of variables by the corresponding entry in `A`, we get `A` back.
More concisely: For any finite type m, commutative semirings R and S, algebra structures on R and S, and a matrix A with entries in S, the algebra homomorphism from multivariate polynomials over m to S induced by the map that maps a pair of indices to the corresponding entry in A, evaluates multivariate polynomials in A to the original matrix A.
|
Matrix.mvPolynomialX_map_eval₂
theorem Matrix.mvPolynomialX_map_eval₂ :
∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
(f : R →+* S) (A : Matrix m n S),
(Matrix.mvPolynomialX m n R).map (MvPolynomial.eval₂ f fun p => A p.1 p.2) = A
This theorem states that any given matrix `A` can be expressed as the evaluation of `Matrix.mvPolynomialX` using the `MvPolynomial.eval₂` function. In particular, this is useful when `MvPolynomial (m × n) R` is an integral domain but `S` is not. In such scenarios, if `MvPolynomial.eval₂` can be pulled to the outer layer of a goal, it can assist with solving the goal under cancellative assumptions. Specifically, for any commutative semirings `R` and `S`, a ring homomorphism from `R` to `S`, and a matrix `A` with elements in `S`, the theorem verifies that mapping the function `MvPolynomial.eval₂` to `Matrix.mvPolynomialX` yields the original matrix `A`.
More concisely: For any commutative semirings R and S, a ring homomorphism from R to S, and a matrix A with elements in S, the evaluation of `Matrix.mvPolynomialX` using `MvPolynomial.eval₂` equals matrix A.
|
Matrix.det_mvPolynomialX_ne_zero
theorem Matrix.det_mvPolynomialX_ne_zero :
∀ (m : Type u_1) (R : Type u_3) [inst : DecidableEq m] [inst_1 : Fintype m] [inst_2 : CommRing R]
[inst_3 : Nontrivial R], (Matrix.mvPolynomialX m m R).det ≠ 0
This theorem states that for any nontrivial commutative ring `R` and any type `m` with decidable equality and finite type, the determinant of the matrix defined by `Matrix.mvPolynomialX m m R` is not zero. In other words, in a nontrivial ring, the determinant of the matrix whose elements are multivariate polynomials with indices as variables is never zero.
More concisely: In a nontrivial commutative ring, the determinant of the matrix of multivariate polynomials with finite type indices is never zero.
|
Matrix.mvPolynomialX_mapMatrix_eval
theorem Matrix.mvPolynomialX_mapMatrix_eval :
∀ {m : Type u_1} {R : Type u_3} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : CommSemiring R]
(A : Matrix m m R), (MvPolynomial.eval fun p => A p.1 p.2).mapMatrix (Matrix.mvPolynomialX m m R) = A
This theorem states that for any finite type `m` and commutative semiring `R`, and given `DecidableEq m` (which asserts that equality between elements of type `m` is decidable), for any matrix `A` of type `Matrix m m R`, the evaluation of a multivariate polynomial using a function that maps a pair of indices `(p.1, p.2)` to the corresponding entry in `A` and subsequent transformation using `mapMatrix` applied to the matrix of multivariate polynomials with variables at each location `(i, j)`, gives back the original matrix `A`. In other words, it asserts that evaluating and then mapping the matrix of multivariate polynomials with variables at each location to a matrix of ring elements, under a particular evaluation map, retrieves the original matrix of ring elements.
More concisely: Given a finite type `m`, a commutative semiring `R` with decidable equality, and a matrix `A` of type `Matrix m m R`, the application of `mapMatrix` to the matrix of multivariate polynomials evaluating to `A` using an evaluation map that corresponds to the entries of `A`, results in `A`.
|