trace_permutation — Mathlib

English

The action of a permutation matrix on a vector is given by the composition with the permutation.

Русский

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

LaTeX

$$$\\sigma\\text{.permMatrix }R \\cdot v = v \\circ \\sigma$$$

Lean4

/-- The trace of a permutation matrix equals the number of fixed points. -/
theorem trace_permutation [AddCommMonoidWithOne R] : trace (σ.permMatrix R) = (Function.fixedPoints σ).ncard :=
  by
  delta trace
  simp [toPEquiv_apply, ← Set.ncard_coe_finset, Function.fixedPoints, Function.IsFixedPt]

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