Theorems · Definition · linear algebra

AddMonoidHom.mapMatrix

{m : Type u_2} →
  {n : Type u_3} →
    {α : Type u_11} →
      {β : Type u_12} → [inst : AddZeroClass α] → [inst_1 : AddZeroClass β] → (α →+ β) → Matrix m n α →+ Matrix m n β

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

Defined in

Mathlib.Data.Matrix.Basic

Cited by

9 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext, Quot.sound

Assumes

AddZeroClassAddZeroClass