conjTranspose_permMatrix — Mathlib

English

For permutation matrices over a star-ring, the conjugate transpose equals the permutation matrix of the inverse permutation.

Русский

Для матриц перестановки над звёздочным кольцом сопряжённое транспонирование даёт матрицу перестановки для обратной перестановки.

LaTeX

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

Lean4

@[simp]
theorem conjTranspose_permMatrix [NonAssocSemiring R] [StarRing R] :
    (σ.permMatrix R).conjTranspose = (σ⁻¹).permMatrix R :=
  by
  simp only [conjTranspose, transpose_permMatrix, map]
  aesop

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