Theorems · Definition · linear algebra

RingHom.mapMatrix

{m : Type u_2} →
  {α : Type u_11} →
    {β : Type u_12} →
      [inst : Fintype m] →
        [inst_1 : DecidableEq m] →
          [inst_2 : NonAssocSemiring α] → [inst_3 : NonAssocSemiring β] → (α →+* β) → Matrix m m α →+* Matrix m m β

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

Defined in

Mathlib.Data.Matrix.Basic

Cited by

55 results in Mathlib

Foundations

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

Assumes

FintypeDecidableEqNonAssocSemiringNonAssocSemiring