Stirling numbers of the first kind

The Stirling numbers of the first kind, defined here as the number of permutations of a finite set with a given number of cycles.

For additional information, refer to https://en.wikipedia.org/wiki/Stirling_numbers_of_the_first_kind.

@[reducible, inline]

abbrev LeanPool.PolyaEnumerationTheorem.StirlingFirstKindSum.stirlingFirstKind (n i : ℕ) : ℕ

The Stirling number of the first kind stirlingFirstKind n i represents the number of permutations of Fin n with exactly i cycles.

Equations

• LeanPool.PolyaEnumerationTheorem.StirlingFirstKindSum.stirlingFirstKind n i = LeanPool.PolyaEnumerationTheorem.CyclesOfGroupElements.numGroupOfNumCycles (Fin n) (Equiv.Perm (Fin n)) i