det_permutation — Mathlib

English

The trace of a permutation matrix equals the number of fixed points of the permutation.

Русский

След матрицы перестановки равен числу фиксированных точек перестановки.

LaTeX

$$$\\operatorname{tr}(\\sigma\\text{ -permMatrix }R) = (\\text{fixedPoints } \\sigma).\\n{\\#} \\text{points}$$$

Lean4

/-- The determinant of a permutation matrix equals its sign. -/
@[simp]
theorem det_permutation [CommRing R] : det (σ.permMatrix R) = Perm.sign σ := by
  rw [← Matrix.mul_one (σ.permMatrix R), PEquiv.toMatrix_toPEquiv_mul, det_permute, det_one, mul_one]

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