matPolyEquiv_coeff_apply

theorem matPolyEquiv_coeff_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type w} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (m : Matrix n n (Polynomial R)) (k : ℕ) (i j : n), (matPolyEquiv m).coeff k i j = (m i j).coeff k

This theorem, `matPolyEquiv_coeff_apply`, states that for any commutative semiring `R`, any type `n` with decidable equality and which is finite (i.e., it has a finite number of elements), any matrix `m` with entries being polynomials over `R` and indexed by `n`, any natural number `k`, and any two indices `i` and `j` of type `n`, the coefficient of `X^k` in the polynomial located at the `(i, j)` entry of the matrix after applying the `matPolyEquiv` function is the same as the coefficient of `X^k` in the polynomial at the `(i, j)` entry of the original matrix `m`. In other words, applying `matPolyEquiv` to a matrix of polynomials doesn't change the coefficients of the individual polynomials.

More concisely: For any commutative semiring R, finite type n with decidable equality, matrix m of polynomials over R indexed by n, natural number k, and indices i and j of type n, the coefficient of X^k in the polynomial at (i, j) in the original matrix m equals the coefficient of X^k in the polynomial at (i, j) in the matrix m obtained by applying matPolyEquiv.