permMatrix — Mathlib

English

A permutation matrix is the matrix associated with a permutation; it has ones in positions corresponding to the permutation and zeros elsewhere.

Русский

Матрица перестановки — матрица, связанная с перестановкой; в её положениях соответствуют перестановке единицы, во всех остальных местах нули.

LaTeX

$$A_\\sigma := (\\sigma\\text{ to matrix}) with entries (A_\\sigma)_{ij} = δ_{i,σ(j)}$$

Lean4

/-- the permutation matrix associated with an `Equiv.Perm` -/
abbrev permMatrix [Zero R] [One R] : Matrix n n R :=
  σ.toPEquiv.toMatrix

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