toMatrix_toPEquiv_eq — Mathlib

English

The permutation matrix P_σ associated to a permutation σ is obtained by permuting the rows of the identity matrix by σ: P_σ = I_n with rows permuted according to σ.

Русский

Связанная с перестановкой матрица P_σ получается перестановкой строк тождественной матрицы I_n по σ.

LaTeX

$$$P_\\sigma = I_n \\text{ with rows permuted by } \\sigma$$$

Lean4

/-- We can also define permutation matrices by permuting the rows of the identity matrix. -/
theorem toMatrix_toPEquiv_eq [DecidableEq n] [Zero α] [One α] (σ : Equiv.Perm n) :
    σ.toPEquiv.toMatrix = (1 : Matrix n n α).submatrix σ id :=
  Matrix.ext fun _ _ => if_congr Option.some_inj rfl rfl

Похожие утверждения