card_fixedPoints — Mathlib

English

The number of fixed points of σ equals the size of the domain minus the total cycle length sum: card(FixPoints(σ)) = |α| − cycleType(σ).sum.

Русский

Число фиксированных точек перестановки σ равно размеру множества минус сумма длин циклов: card(FixPoints(σ)) = |α| − cycleType(σ).sum.

LaTeX

$$$$|\mathrm{FixPoints}(\sigma)| = |\alpha| - \mathrm{cycleType}(\sigma).sum.$$$$

Lean4

theorem card_fixedPoints (σ : Equiv.Perm α) :
    Fintype.card (Function.fixedPoints σ) = Fintype.card α - σ.cycleType.sum :=
  by
  rw [Equiv.Perm.sum_cycleType, ← Finset.card_compl, Fintype.card_ofFinset]
  congr; aesop

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