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