Theorems · Definition · linear algebra

Matrix.reindexLinearEquiv

{m : Type u_2} →
  {n : Type u_3} →
    {m' : Type u_6} →
      {n' : Type u_7} →
        (R : Type u_11) →
          (A : Type u_12) →
            [inst : Semiring R] →
              [inst_1 : AddCommMonoid A] → [inst_2 : Module R A] → m ≃ m' → n ≃ n' → Matrix m n A ≃ₗ[R] Matrix m' n' A

The natural map that reindexes a matrix's rows and columns with equivalent types, Matrix.reindex, is a linear equivalence.

Defined in

Mathlib.LinearAlgebra.Matrix.Reindex

Cited by

18 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModule