mathlib documentation

linear_algebra.matrix.reindex

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 #

Tags #

matrix, reindex

def matrix.reindex_linear_equiv {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {m' : Type u_5} {n' : Type u_6} [fintype m'] [fintype n'] {R : Type u_7} [semiring R] (eₘ : m m') (eₙ : n n') :
matrix m n R ≃ₗ[R] matrix m' n' R

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

Equations
@[simp]
theorem matrix.reindex_linear_equiv_apply {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {m' : Type u_5} {n' : Type u_6} [fintype m'] [fintype n'] {R : Type u_7} [semiring R] (eₘ : m m') (eₙ : n n') (M : matrix m n R) :
@[simp]
theorem matrix.reindex_linear_equiv_symm {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {m' : Type u_5} {n' : Type u_6} [fintype m'] [fintype n'] {R : Type u_7} [semiring R] (eₘ : m m') (eₙ : n n') :
@[simp]
theorem matrix.reindex_linear_equiv_refl_refl {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {R : Type u_7} [semiring R] :
theorem matrix.reindex_linear_equiv_mul {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {m' : Type u_5} {n' : Type u_6} [fintype m'] [fintype n'] {R : Type u_7} {o : Type u_1} {o' : Type u_4} [fintype o] [fintype o'] [semiring R] (eₘ : m m') (eₙ : n n') (eₒ : o o') (M : matrix m n R) (N : matrix n o R) :
def matrix.reindex_alg_equiv {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {R : Type u_7} [comm_semiring R] [decidable_eq m] [decidable_eq n] (e : m n) :
matrix m m R ≃ₐ[R] matrix n n R

For square matrices, the natural map that reindexes a matrix's rows and columns with equivalent types, matrix.reindex, is an equivalence of algebras.

Equations
@[simp]
theorem matrix.reindex_alg_equiv_apply {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {R : Type u_7} [comm_semiring R] [decidable_eq m] [decidable_eq n] (e : m n) (M : matrix m m R) :
@[simp]
theorem matrix.reindex_alg_equiv_symm {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {R : Type u_7} [comm_semiring R] [decidable_eq m] [decidable_eq n] (e : m n) :
theorem matrix.reindex_alg_equiv_mul {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {R : Type u_7} [comm_semiring R] [decidable_eq m] [decidable_eq n] (e : m n) (M N : matrix m m R) :
theorem matrix.det_reindex_linear_equiv_self {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {R : Type u_7} [decidable_eq m] [decidable_eq n] [comm_ring R] (e : m n) (A : matrix m m R) :

Reindexing both indices along the same equivalence preserves the determinant.

For the simp version of this lemma, see det_minor_equiv_self.

theorem matrix.det_reindex_alg_equiv {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {R : Type u_7} [decidable_eq m] [decidable_eq n] [comm_ring R] (e : m n) (A : matrix m m R) :

Reindexing both indices along the same equivalence preserves the determinant.

For the simp version of this lemma, see det_minor_equiv_self.