Matrix reindexing by permutations

Identities for Matrix.reindex when acting symmetrically on rows and columns by permutations: composition with respect to permutation multiplication, identity action, and pointwise characterization.

Main results

• Matrix.reindex_perm_mul: reindex (σ * τ) (σ * τ) M = reindex σ σ (reindex τ τ M).
• Matrix.reindex_perm_one: reindex 1 1 M = M.
• Matrix.reindex_eq_iff: reindex eₘ eₙ A = M ↔ ∀ i j, M (eₘ i) (eₙ j) = A i j.

theorem Matrix.reindex_perm_mul {m : Type u_1} {α : Type u_5} (σ τ : Equiv.Perm m) (M : Matrix m m α) : (reindex (σ * τ) (σ * τ)) M = (reindex σ σ) ((reindex τ τ) M)

Relabelling a square matrix by a product of permutations is relabelling twice.

theorem Matrix.reindex_perm_one {m : Type u_1} {α : Type u_5} (M : Matrix m m α) : (reindex 1 1) M = M

Relabelling by the identity permutation does nothing.

theorem Matrix.reindex_eq_iff {m : Type u_1} {n : Type u_2} {l : Type u_3} {o : Type u_4} {α : Type u_5} {eₘ : m ≃ l} {eₙ : n ≃ o} {A : Matrix m n α} {M : Matrix l o α} : (reindex eₘ eₙ) A = M ↔ ∀ (i : m) (j : n), M (eₘ i) (eₙ j) = A i j

Matrix.reindex eₘ eₙ A = M says that (eₘ, eₙ) carries A to M.