English
For a finite m, there is a canonical correspondence between a matrix M and a submatrix representation under a permutation f: M * f.toPEquiv.toMatrix equals M.submatrix id f.symm.
Русский
Существует естественное соответствие между матрицей M и её представлением через перестановку: M * f.toPEquiv.toMatrix = M.submatrix id f.symm.
LaTeX
$$$\\text{Let } M \\in M_{m\\times n}(α), \\; f: m \\simeq n.\\quad M * f.toPEquiv.toMatrix = M.submatrix id (f^{-1}).$$$
Lean4
/-- `toMatrix` returns a matrix containing ones and zeros. `f.toMatrix i j` is `1` if
`f i = some j` and `0` otherwise -/
def toMatrix [DecidableEq n] [Zero α] [One α] (f : m ≃. n) : Matrix m n α :=
of fun i j =>
if j ∈ f i then (1 : α)
else
0
-- TODO: set as an equation lemma for `toMatrix`, see https://github.com/leanprover-community/mathlib4/pull/3024
