Changing the index type of a matrix #

This file concerns the map Matrix.reindex, mapping a m by n matrix to an m' by n' matrix, as long as m ≃ m' and n ≃ n'.

Main definitions #

Matrix.reindexAddEquiv R: Matrix.reindex as an AddEquiv between R-matrices.
Matrix.reindexRingEquiv R: Matrix.reindex as a RingEquiv between R-matrices.
Matrix.reindexLinearEquiv R A: Matrix.reindex is an R-linear equivalence between A-matrices.
Matrix.reindexAlgEquiv R A: Matrix.reindex is an R-algebra equivalence between A-matrices.

Tags #

matrix, reindex

source

def Matrix.reindexAddEquiv {m : Type u_2} {n : Type u_3} {m' : Type u_6} {n' : Type u_7} (R : Type u_11) [Add R] (eₘ : m ≃ m') (eₙ : n ≃ n') :

Matrix m n R ≃+ Matrix m' n' R

Matrix.reindex as an AddEquiv between R-matrices.

Equations

Matrix.reindexAddEquiv R eₘ eₙ = { toEquiv := Matrix.reindex eₘ eₙ, map_add' := ⋯ }

Instances For

source

@[simp]

theorem Matrix.coe_reindexAddEquiv {m : Type u_2} {n : Type u_3} {m' : Type u_6} {n' : Type u_7} (R : Type u_11) [Add R] (eₘ : m ≃ m') (eₙ : n ≃ n') :

⇑(reindexAddEquiv R eₘ eₙ) = ⇑(reindex eₘ eₙ)

source

@[simp]

theorem Matrix.toEquiv_reindexAddEquiv {m : Type u_2} {n : Type u_3} {m' : Type u_6} {n' : Type u_7} (R : Type u_11) [Add R] (eₘ : m ≃ m') (eₙ : n ≃ n') :

↑(reindexAddEquiv R eₘ eₙ) = reindex eₘ eₙ

source

@[simp]

theorem Matrix.symm_reindexAddEquiv {m : Type u_2} {n : Type u_3} {m' : Type u_6} {n' : Type u_7} (R : Type u_11) [Add R] (eₘ : m ≃ m') (eₙ : n ≃ n') :

(reindexAddEquiv R eₘ eₙ).symm = reindexAddEquiv R eₘ.symm eₙ.symm

source

@[simp]

theorem Matrix.reindexAddEquiv_refl_refl {m : Type u_2} {n : Type u_3} (R : Type u_11) [Add R] :

reindexAddEquiv R (Equiv.refl m) (Equiv.refl n) = AddEquiv.refl (Matrix m n R)

source

@[simp]

theorem Matrix.reindexAddEquiv_trans_reindexAddEquiv {m : Type u_2} {n : Type u_3} {m' : Type u_6} {n' : Type u_7} {m'' : Type u_9} {n'' : Type u_10} (R : Type u_11) [Add R] (e₁ : m ≃ m') (e₂ : n ≃ n') (e₁' : m' ≃ m'') (e₂' : n' ≃ n'') :

(reindexAddEquiv R e₁ e₂).trans (reindexAddEquiv R e₁' e₂') = reindexAddEquiv R (e₁.trans e₁') (e₂.trans e₂')

source

def Matrix.reindexRingEquiv {m : Type u_2} {n : Type u_3} (R : Type u_11) [Fintype m] [Fintype n] [Mul R] [AddCommMonoid R] (e : m ≃ n) :

Matrix m m R ≃+* Matrix n n R

Matrix.reindex as a RingEquiv between R-matrices.

Equations

Matrix.reindexRingEquiv R e = { toEquiv := (Matrix.reindexAddEquiv R e e).toEquiv, map_mul' := ⋯, map_add' := ⋯ }

Instances For

source

@[simp]

theorem Matrix.coe_reindexRingEquiv {m : Type u_2} {n : Type u_3} (R : Type u_11) [Fintype m] [Fintype n] [Mul R] [AddCommMonoid R] (e : m ≃ n) :

⇑(reindexRingEquiv R e) = ⇑(reindex e e)

source

@[simp]

theorem Matrix.toEquiv_reindexRingEquiv {m : Type u_2} {n : Type u_3} (R : Type u_11) [Fintype m] [Fintype n] [Mul R] [AddCommMonoid R] (e : m ≃ n) :

↑(reindexRingEquiv R e) = reindex e e

source

@[simp]

theorem Matrix.toAddEquiv_reindexRingEquiv {m : Type u_2} {n : Type u_3} (R : Type u_11) [Fintype m] [Fintype n] [Mul R] [AddCommMonoid R] (e : m ≃ n) :

↑(reindexRingEquiv R e) = reindexAddEquiv R e e

source

@[simp]

theorem Matrix.symm_reindexRingEquiv {m : Type u_2} {n : Type u_3} (R : Type u_11) [Fintype m] [Fintype n] [Mul R] [AddCommMonoid R] (e : m ≃ n) :

(reindexRingEquiv R e).symm = reindexRingEquiv R e.symm

source

@[simp]

theorem Matrix.reindexRingEquiv_refl {n : Type u_3} (R : Type u_11) [Fintype n] [Mul R] [AddCommMonoid R] :

reindexRingEquiv R (Equiv.refl n) = RingEquiv.refl (Matrix n n R)

source

@[simp]

theorem Matrix.reindexRingEquiv_trans_reindexRingEquiv {m : Type u_2} {n : Type u_3} {o : Type u_4} (R : Type u_11) [Fintype m] [Fintype n] [Fintype o] [Mul R] [AddCommMonoid R] (e : m ≃ n) (e' : n ≃ o) :

(reindexRingEquiv R e).trans (reindexRingEquiv R e') = reindexRingEquiv R (e.trans e')

source

def 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) [Semiring R] [AddCommMonoid A] [Module R A] (eₘ : m ≃ m') (eₙ : 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.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem Matrix.coe_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) [Semiring R] [AddCommMonoid A] [Module R A] (eₘ : m ≃ m') (eₙ : n ≃ n') :

⇑(reindexLinearEquiv R A eₘ eₙ) = ⇑(reindex eₘ eₙ)

source

@[simp]

theorem Matrix.toEquiv_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) [Semiring R] [AddCommMonoid A] [Module R A] (eₘ : m ≃ m') (eₙ : n ≃ n') :

↑(reindexLinearEquiv R A eₘ eₙ) = reindex eₘ eₙ

source

@[simp]

theorem Matrix.toAddEquiv_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) [Semiring R] [AddCommMonoid A] [Module R A] (eₘ : m ≃ m') (eₙ : n ≃ n') :

↑(reindexLinearEquiv R A eₘ eₙ) = reindexAddEquiv A eₘ eₙ

source

@[deprecated Matrix.coe_reindexLinearEquiv (since := "2026-06-06")]

theorem Matrix.reindexLinearEquiv_apply {m : Type u_2} {n : Type u_3} {m' : Type u_6} {n' : Type u_7} (R : Type u_11) (A : Type u_12) [Semiring R] [AddCommMonoid A] [Module R A] (eₘ : m ≃ m') (eₙ : n ≃ n') (M : Matrix m n A) :

(reindexLinearEquiv R A eₘ eₙ) M = (reindex eₘ eₙ) M

source

@[simp]

theorem Matrix.symm_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) [Semiring R] [AddCommMonoid A] [Module R A] (eₘ : m ≃ m') (eₙ : n ≃ n') :

(reindexLinearEquiv R A eₘ eₙ).symm = reindexLinearEquiv R A eₘ.symm eₙ.symm

source

@[deprecated Matrix.symm_reindexLinearEquiv (since := "2026-06-06")]

theorem Matrix.reindexLinearEquiv_symm {m : Type u_2} {n : Type u_3} {m' : Type u_6} {n' : Type u_7} (R : Type u_11) (A : Type u_12) [Semiring R] [AddCommMonoid A] [Module R A] (eₘ : m ≃ m') (eₙ : n ≃ n') :

(reindexLinearEquiv R A eₘ eₙ).symm = reindexLinearEquiv R A eₘ.symm eₙ.symm

Alias of Matrix.symm_reindexLinearEquiv.

source

@[simp]

theorem Matrix.reindexLinearEquiv_refl_refl {m : Type u_2} {n : Type u_3} (R : Type u_11) (A : Type u_12) [Semiring R] [AddCommMonoid A] [Module R A] :

reindexLinearEquiv R A (Equiv.refl m) (Equiv.refl n) = LinearEquiv.refl R (Matrix m n A)

source

@[simp]

theorem Matrix.reindexLinearEquiv_trans_reindexLinearEquiv {m : Type u_2} {n : Type u_3} {m' : Type u_6} {n' : Type u_7} {m'' : Type u_9} {n'' : Type u_10} (R : Type u_11) (A : Type u_12) [Semiring R] [AddCommMonoid A] [Module R A] (e₁ : m ≃ m') (e₂ : n ≃ n') (e₁' : m' ≃ m'') (e₂' : n' ≃ n'') :

reindexLinearEquiv R A e₁ e₂ ≪≫ₗ reindexLinearEquiv R A e₁' e₂' = reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂')

source

@[deprecated Matrix.reindexLinearEquiv_trans_reindexLinearEquiv (since := "2026-06-06")]

theorem Matrix.reindexLinearEquiv_trans {m : Type u_2} {n : Type u_3} {m' : Type u_6} {n' : Type u_7} {m'' : Type u_9} {n'' : Type u_10} (R : Type u_11) (A : Type u_12) [Semiring R] [AddCommMonoid A] [Module R A] (e₁ : m ≃ m') (e₂ : n ≃ n') (e₁' : m' ≃ m'') (e₂' : n' ≃ n'') :

reindexLinearEquiv R A e₁ e₂ ≪≫ₗ reindexLinearEquiv R A e₁' e₂' = reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂')

Alias of Matrix.reindexLinearEquiv_trans_reindexLinearEquiv.

source

theorem Matrix.reindexLinearEquiv_comp {m : Type u_2} {n : Type u_3} {m' : Type u_6} {n' : Type u_7} {m'' : Type u_9} {n'' : Type u_10} (R : Type u_11) (A : Type u_12) [Semiring R] [AddCommMonoid A] [Module R A] (e₁ : m ≃ m') (e₂ : n ≃ n') (e₁' : m' ≃ m'') (e₂' : n' ≃ n'') :

⇑(reindexLinearEquiv R A e₁' e₂') ∘ ⇑(reindexLinearEquiv R A e₁ e₂) = ⇑(reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂'))

source

theorem Matrix.reindexLinearEquiv_comp_apply {m : Type u_2} {n : Type u_3} {m' : Type u_6} {n' : Type u_7} {m'' : Type u_9} {n'' : Type u_10} (R : Type u_11) (A : Type u_12) [Semiring R] [AddCommMonoid A] [Module R A] (e₁ : m ≃ m') (e₂ : n ≃ n') (e₁' : m' ≃ m'') (e₂' : n' ≃ n'') (M : Matrix m n A) :

(reindexLinearEquiv R A e₁' e₂') ((reindexLinearEquiv R A e₁ e₂) M) = (reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂')) M

source

theorem Matrix.reindexLinearEquiv_one {m : Type u_2} {m' : Type u_6} (R : Type u_11) (A : Type u_12) [Semiring R] [AddCommMonoid A] [Module R A] [DecidableEq m] [DecidableEq m'] [One A] (e : m ≃ m') :

(reindexLinearEquiv R A e e) 1 = 1

source

theorem Matrix.reindexLinearEquiv_mul {m : Type u_2} {n : Type u_3} {o : Type u_4} {m' : Type u_6} {n' : Type u_7} {o' : Type u_8} (R : Type u_11) (A : Type u_12) [Semiring R] [Semiring A] [Module R A] [Fintype n] [Fintype n'] (eₘ : m ≃ m') (eₙ : n ≃ n') (eₒ : o ≃ o') (M : Matrix m n A) (N : Matrix n o A) :

(reindexLinearEquiv R A eₘ eₙ) M * (reindexLinearEquiv R A eₙ eₒ) N = (reindexLinearEquiv R A eₘ eₒ) (M * N)

source

theorem Matrix.mul_reindexLinearEquiv_one {m : Type u_2} {n : Type u_3} {o : Type u_4} {n' : Type u_7} (R : Type u_11) (A : Type u_12) [Semiring R] [Semiring A] [Module R A] [Fintype n] [DecidableEq o] (e₁ : o ≃ n) (e₂ : o ≃ n') (M : Matrix m n A) :

M * (reindexLinearEquiv R A e₁ e₂) 1 = (reindexLinearEquiv R A (Equiv.refl m) (e₁.symm.trans e₂)) M

source

def Matrix.reindexAlgEquiv {m : Type u_2} {n : Type u_3} (R : Type u_11) (A : Type u_12) [CommSemiring R] [Fintype n] [Fintype m] [DecidableEq m] [DecidableEq n] [Semiring A] [Algebra R A] (e : m ≃ n) :

Matrix m m A ≃ₐ[R] Matrix n n A

For square matrices with coefficients in an algebra over a commutative semiring, the natural map that reindexes a matrix's rows and columns with equivalent types, Matrix.reindex, is an equivalence of algebras.

Equations

Matrix.reindexAlgEquiv R A e = { toEquiv := (Matrix.reindexRingEquiv A e).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

Instances For

source

@[simp]

theorem Matrix.coe_reindexAlgEquiv {m : Type u_2} {n : Type u_3} (R : Type u_11) (A : Type u_12) [CommSemiring R] [Fintype n] [Fintype m] [DecidableEq m] [DecidableEq n] [Semiring A] [Algebra R A] (e : m ≃ n) :

⇑(reindexAlgEquiv R A e) = ⇑(reindex e e)

source

@[simp]

theorem Matrix.toEquiv_reindexAlgEquiv {m : Type u_2} {n : Type u_3} (R : Type u_11) (A : Type u_12) [CommSemiring R] [Fintype n] [Fintype m] [DecidableEq m] [DecidableEq n] [Semiring A] [Algebra R A] (e : m ≃ n) :

↑(reindexAlgEquiv R A e) = reindex e e

source

@[simp]

theorem Matrix.toAddEquiv_reindexAlgEquiv {m : Type u_2} {n : Type u_3} (R : Type u_11) (A : Type u_12) [CommSemiring R] [Fintype n] [Fintype m] [DecidableEq m] [DecidableEq n] [Semiring A] [Algebra R A] (e : m ≃ n) :

↑(reindexAlgEquiv R A e) = reindexAddEquiv A e e

source

@[simp]

theorem Matrix.toRingEquiv_reindexAlgEquiv {m : Type u_2} {n : Type u_3} (R : Type u_11) (A : Type u_12) [CommSemiring R] [Fintype n] [Fintype m] [DecidableEq m] [DecidableEq n] [Semiring A] [Algebra R A] (e : m ≃ n) :

(reindexAlgEquiv R A e).toRingEquiv = reindexRingEquiv A e

source

@[simp]

theorem Matrix.toLinearEquiv_reindexAlgEquiv {m : Type u_2} {n : Type u_3} (R : Type u_11) (A : Type u_12) [CommSemiring R] [Fintype n] [Fintype m] [DecidableEq m] [DecidableEq n] [Semiring A] [Algebra R A] (e : m ≃ n) :

↑(reindexAlgEquiv R A e) = reindexLinearEquiv R A e e

source

@[deprecated Matrix.coe_reindexAlgEquiv (since := "2026-06-06")]

theorem Matrix.reindexAlgEquiv_apply {m : Type u_2} {n : Type u_3} (R : Type u_11) (A : Type u_12) [CommSemiring R] [Fintype n] [Fintype m] [DecidableEq m] [DecidableEq n] [Semiring A] [Algebra R A] (e : m ≃ n) (M : Matrix m m A) :

(reindexAlgEquiv R A e) M = (reindex e e) M

source

@[simp]

theorem Matrix.symm_reindexAlgEquiv {m : Type u_2} {n : Type u_3} (R : Type u_11) (A : Type u_12) [CommSemiring R] [Fintype n] [Fintype m] [DecidableEq m] [DecidableEq n] [Semiring A] [Algebra R A] (e : m ≃ n) :

(reindexAlgEquiv R A e).symm = reindexAlgEquiv R A e.symm

source

@[deprecated Matrix.symm_reindexAlgEquiv (since := "2026-06-06")]

theorem Matrix.reindexAlgEquiv_symm {m : Type u_2} {n : Type u_3} (R : Type u_11) (A : Type u_12) [CommSemiring R] [Fintype n] [Fintype m] [DecidableEq m] [DecidableEq n] [Semiring A] [Algebra R A] (e : m ≃ n) :

(reindexAlgEquiv R A e).symm = reindexAlgEquiv R A e.symm

Alias of Matrix.symm_reindexAlgEquiv.

source

@[simp]

theorem Matrix.reindexAlgEquiv_refl {m : Type u_2} (R : Type u_11) (A : Type u_12) [CommSemiring R] [Fintype m] [DecidableEq m] [Semiring A] [Algebra R A] :

reindexAlgEquiv R A (Equiv.refl m) = AlgEquiv.refl

source

@[simp]

theorem Matrix.reindexAlgEquiv_trans_reindexAlgEquiv {m : Type u_2} {n : Type u_3} {o : Type u_4} (R : Type u_11) (A : Type u_12) [CommSemiring R] [Fintype n] [Fintype m] [Fintype o] [DecidableEq m] [DecidableEq n] [DecidableEq o] [Semiring A] [Algebra R A] (e : m ≃ n) (e' : n ≃ o) :

(reindexAlgEquiv R A e).trans (reindexAlgEquiv R A e') = reindexAlgEquiv R A (e.trans e')

source

@[deprecated map_mul (since := "2026-06-06")]

theorem Matrix.reindexAlgEquiv_mul {m : Type u_2} {n : Type u_3} (R : Type u_11) (A : Type u_12) [CommSemiring R] [Fintype n] [Fintype m] [DecidableEq m] [DecidableEq n] [Semiring A] [Algebra R A] (e : m ≃ n) (M N : Matrix m m A) :

(reindexAlgEquiv R A e) (M * N) = (reindexAlgEquiv R A e) M * (reindexAlgEquiv R A e) N

source

theorem Matrix.det_reindexLinearEquiv_self {m : Type u_2} {n : Type u_3} (R : Type u_11) [CommRing R] [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] (e : m ≃ n) (M : Matrix m m R) :

((reindexLinearEquiv R R e e) M).det = M.det

Reindexing both indices along the same equivalence preserves the determinant.

For the simp version of this lemma, see det_submatrix_equiv_self.

source

theorem Matrix.det_reindexAlgEquiv {m : Type u_2} {n : Type u_3} (R : Type u_11) (B : Type u_13) [CommSemiring R] [CommRing B] [Algebra R B] [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] (e : m ≃ n) (A : Matrix m m B) :

((reindexAlgEquiv R B e) A).det = A.det

Reindexing both indices along the same equivalence preserves the determinant.

For the simp version of this lemma, see det_submatrix_equiv_self.

Documentation

Mathlib.LinearAlgebra.Matrix.Reindex

Changing the index type of a matrix #

Main definitions #

Tags #