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 α] :
to_matrix returns a matrix containing ones and zeros. f.to_matrix i j is 1 if
f i = some j and 0 otherwise
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 α] :
(pequiv.refl n).to_matrix = 1
@[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) :
(equiv.to_pequiv (equiv.swap i j)).to_matrix = 1 - (pequiv.single i i).to_matrix - (pequiv.single j j).to_matrix + (pequiv.single i j).to_matrix + (pequiv.single j i).to_matrix
@[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) :
(pequiv.single a b).to_matrix.mul (pequiv.single b c).to_matrix = (pequiv.single a c).to_matrix
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) :
(pequiv.single a b₁).to_matrix.mul (pequiv.single b₂ c).to_matrix = 0
@[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 α) :
(pequiv.single a b).to_matrix.mul ((pequiv.single b c).to_matrix.mul M) = (pequiv.single a c).to_matrix.mul M
Restatement of single_mul_single, which will simplify expressions in simp normal form,
when associativity may otherwise need to be carefully applied.