mathlib documentation

data.matrix.pequiv

def pequiv.to_matrix {m : Type u_3} {n : Type u_4} [fintype m] [fintype n] {α : Type v} [decidable_eq n] [has_zero α] [has_one α] :
(m ≃. n)matrix m n α

to_matrix returns a matrix containing ones and zeros. f.to_matrix i j is 1 if f i = some j and 0 otherwise

Equations
theorem pequiv.mul_matrix_apply {l : Type u_2} {m : Type u_3} {n : Type u_4} [fintype l] [fintype m] [fintype n] {α : Type v} [decidable_eq m] [semiring α] (f : l ≃. m) (M : matrix m n α) (i : l) (j : n) :
(f.to_matrix M) i j = (f i).cases_on 0 (λ (fi : m), M fi j)

theorem pequiv.to_matrix_symm {m : Type u_3} {n : Type u_4} [fintype m] [fintype n] {α : Type v} [decidable_eq m] [decidable_eq n] [has_zero α] [has_one α] (f : m ≃. n) :

@[simp]
theorem pequiv.to_matrix_refl {n : Type u_4} [fintype n] {α : Type v} [decidable_eq n] [has_zero α] [has_one α] :

theorem pequiv.matrix_mul_apply {l : Type u_2} {m : Type u_3} {n : Type u_4} [fintype l] [fintype m] [fintype n] {α : Type v} [semiring α] [decidable_eq n] (M : matrix l m α) (f : m ≃. n) (i : l) (j : n) :
(M f.to_matrix) i j = ((f.symm) j).cases_on 0 (λ (fj : m), M i fj)

theorem pequiv.to_pequiv_mul_matrix {m : Type u_3} {n : Type u_4} [fintype m] [fintype n] {α : Type v} [decidable_eq m] [semiring α] (f : m m) (M : matrix m n α) :
f.to_pequiv.to_matrix M = λ (i : m), M (f i)

theorem pequiv.to_matrix_trans {l : Type u_2} {m : Type u_3} {n : Type u_4} [fintype l] [fintype m] [fintype n] {α : Type v} [decidable_eq m] [decidable_eq n] [semiring α] (f : l ≃. m) (g : m ≃. n) :

@[simp]
theorem pequiv.to_matrix_bot {m : Type u_3} {n : Type u_4} [fintype m] [fintype n] {α : Type v} [decidable_eq n] [has_zero α] [has_one α] :

theorem pequiv.to_matrix_injective {m : Type u_3} {n : Type u_4} [fintype m] [fintype n] {α : Type v} [decidable_eq n] [monoid_with_zero α] [nontrivial α] :

theorem pequiv.to_matrix_swap {n : Type u_4} [fintype n] {α : Type v} [decidable_eq n] [ring α] (i j : n) :

@[simp]
theorem pequiv.single_mul_single {k : Type u_1} {m : Type u_3} {n : Type u_4} [fintype k] [fintype m] [fintype n] {α : Type v} [decidable_eq k] [decidable_eq m] [decidable_eq n] [semiring α] (a : m) (b : n) (c : k) :

theorem pequiv.single_mul_single_of_ne {k : Type u_1} {m : Type u_3} {n : Type u_4} [fintype k] [fintype m] [fintype n] {α : Type v} [decidable_eq k] [decidable_eq m] [decidable_eq n] [semiring α] {b₁ b₂ : n} (hb : b₁ b₂) (a : m) (c : k) :

@[simp]
theorem pequiv.single_mul_single_right {k : Type u_1} {l : Type u_2} {m : Type u_3} {n : Type u_4} [fintype k] [fintype l] [fintype m] [fintype n] {α : Type v} [decidable_eq k] [decidable_eq m] [decidable_eq n] [semiring α] (a : m) (b : n) (c : k) (M : matrix k l α) :

Restatement of single_mul_single, which will simplify expressions in simp normal form, when associativity may otherwise need to be carefully applied.

theorem pequiv.equiv_to_pequiv_to_matrix {n : Type u_4} [fintype n] {α : Type v} [decidable_eq n] [has_zero α] [has_one α] (σ : n n) (i j : n) :
σ.to_pequiv.to_matrix i j = 1 (σ i) j

We can also define permutation matrices by permuting the rows of the identity matrix.