PEquiv.single_mul_single_right
theorem PEquiv.single_mul_single_right :
∀ {k : Type u_1} {l : Type u_2} {m : Type u_3} {n : Type u_4} {α : Type v} [inst : Fintype n] [inst_1 : Fintype k]
[inst_2 : DecidableEq n] [inst_3 : DecidableEq k] [inst_4 : DecidableEq m] [inst_5 : Semiring α] (a : m) (b : n)
(c : k) (M : Matrix k l α),
(PEquiv.single a b).toMatrix * ((PEquiv.single b c).toMatrix * M) = (PEquiv.single a c).toMatrix * M
This theorem, known as `PEquiv.single_mul_single_right`, states that, given any types `k`, `l`, `m`, `n`, `α`, where `n` and `k` are of finite type and `α` is a semiring, and given any elements `a` of type `m`, `b` of type `n`, `c` of type `k`, and `M` which is a matrix with entries in `α`, rows indexed by `k` and columns indexed by `l`, the multiplication of the matrix representation of a partial equivalence relation (PEquiv) that sends `a` to `b` with the product of the matrix representation of a PEquiv that sends `b` to `c` and `M` is equal to the multiplication of the matrix representation of a PEquiv that sends `a` to `c` with `M`. This theorem is a restatement of `single_mul_single` and helps simplify expressions in `simp` normal form, especially when associativity may need to be carefully applied.
More concisely: Given matrices `M` of type `α` with rows indexed by a finite type `k` and columns indexed by `l`, and PEquivs `R` and `S` on types `m`, `n`, and `k`, if `R` maps `a` to `b` and `S` maps `b` to `c`, then `R * M * S` equals `M * S * (R |-> c)`.
|
PEquiv.equiv_toPEquiv_toMatrix
theorem PEquiv.equiv_toPEquiv_toMatrix :
∀ {n : Type u_4} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α] [inst_2 : One α] (σ : n ≃ n) (i j : n),
σ.toPEquiv.toMatrix i j = 1 (σ i) j
The theorem `PEquiv.equiv_toPEquiv_toMatrix` states that for any types `n` and `α`, given that `n` has decidable equality, and `α` has a zero and one element, for any permutation `σ` of type `n`, and any two elements `i` and `j` of type `n`, the matrix element at position `(i, j)` of the permutation matrix created by permuting the rows of the identity matrix according to `σ` is equal to 1 if and only if `σ i` equals `j`. This essentially defines a permutation matrix in terms of permutations of the identity matrix's rows.
More concisely: For any permutation σ of type n and any i, j in n with decidable equality on n and zero and one elements in type α, the (i, j)-th entry of the permutation matrix of σ is equal to 1 if and only if σ(i) = j.
|