transpose_permMatrix — Mathlib

English

The transpose of the permutation matrix corresponds to the inverse permutation: (P_σ)^T = P_{σ^{-1}}.

Русский

Транспонированная матрица перестановки соответствует обратной перестановке: (P_σ)^T = P_{σ^{-1}}.

LaTeX

$$$(\\operatorname{permMatrix}(R, \\sigma))^T = \\operatorname{permMatrix}(R, \\sigma^{-1})$$$

Lean4

@[simp]
theorem transpose_permMatrix [Zero R] [One R] : (σ.permMatrix R).transpose = (σ⁻¹).permMatrix R := by
  rw [← PEquiv.toMatrix_symm, ← Equiv.toPEquiv_symm, ← Equiv.Perm.inv_def]

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