instFintype

Mathlib.Combinatorics.Enumerative.Partition

URI: https://scilib.ai/kg/mathlib#Nat.Partition.instFintype

← MathLib Explorer

English

There are finitely many partitions of n.

Русский

Существует конечное число разбиений числа n.

LaTeX

$$$|\mathrm{Partition}(n)| < \infty$$$

Lean4

/-- Show there are finitely many partitions by considering the surjection from compositions to
partitions.
-/
instance (n : ℕ) : Fintype (Partition n) :=
  Fintype.ofSurjective (ofComposition n) ofComposition_surj

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru