Theorems · Definition · linear algebra

matPolyEquiv

{R : Type u_1} →
  [inst : CommSemiring R] →
    {n : Type w} →
      [inst_1 : DecidableEq n] → [inst_2 : Fintype n] → Matrix n n (Polynomial R) ≃ₐ[R] Polynomial (Matrix n n R)

The algebra isomorphism stating "matrices of polynomials are the same as polynomials of matrices". (You probably shouldn't attempt to use this underlying definition it's an algebra equivalence, and characterised extensionally by the lemma matPolyEquiv_coeff_apply below.)

Defined in

Mathlib.RingTheory.MatrixPolynomialAlgebra

Cited by

23 results in Mathlib

Foundations

Depth 120 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringDecidableEqFintype