Theorems · Definition · linear algebra

RingEquiv.mapMatrix

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

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

Defined in

Mathlib.Data.Matrix.Basic

Cited by

6 results in Mathlib

Foundations

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

Assumes

FintypeDecidableEqNonAssocSemiringNonAssocSemiring