instFintypeElemPermDerangements — Mathlib

English

If α is finite (with decidable equality), then the set of derangements on α is finite.

Русский

Если α конечно и для него задано разрешимое равенство, то множество перестановок без фиксаций точек на α является конечно множеством.

LaTeX

$$$\\#\\mathrm{derangements}(\\alpha) < \\infty$ \\. (при [Fintype α])$$

Lean4

instance : Fintype (derangements α) :=
  inferInstanceAs <| Fintype {f : Perm α | ∀ x : α, f x ≠ x}

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