Theorems · Theorem · linear algebra

PEquiv.map_toMatrix

∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} {β : Type u_6} [inst : DecidableEq n] [inst_1 : NonAssocSemiring α]
  [inst_2 : NonAssocSemiring β] (f : α →+* β) (σ : m ≃. n), σ.toMatrix.map ⇑f = σ.toMatrix

Defined in

Mathlib.Data.Matrix.PEquiv

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableEqNonAssocSemiringNonAssocSemiring