Theorems · Definition · linear algebra

Matrix.reindex

{l : Type u_1} →
  {m : Type u_2} → {n : Type u_3} → {o : Type u_4} → {α : Type v} → m ≃ l → n ≃ o → Matrix m n α ≃ Matrix l o α

The natural map that reindexes a matrix's rows and columns with equivalent types is an equivalence.

Defined in

Mathlib.LinearAlgebra.Matrix.Defs

Cited by

102 results in Mathlib

Foundations

Depth 17 from the axioms, rests on 65 definitions · uses propext, Quot.sound