Theorems · Definition · linear algebra

AlgHom.mapMatrix

{m : Type u_2} →
  {R : Type u_7} →
    {α : Type u_11} →
      {β : Type u_12} →
        [inst : Fintype m] →
          [inst_1 : DecidableEq m] →
            [inst_2 : CommSemiring R] →
              [inst_3 : Semiring α] →
                [inst_4 : Semiring β] →
                  [inst_5 : Algebra R α] → [inst_6 : Algebra R β] → (α →ₐ[R] β) → Matrix m m α →ₐ[R] Matrix m m β

The AlgHom between spaces of square matrices induced by an AlgHom between their coefficients. This is Matrix.map as an AlgHom.

Defined in

Mathlib.Data.Matrix.Basic

Cited by

14 results in Mathlib

Foundations

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

Assumes

FintypeDecidableEqCommSemiringSemiringSemiringAlgebraAlgebra