Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-05 08:49 8f4475b4

View on Github →

feat(combinatorics/partitions): Add partitions (#4303)

Estimated changes

Modified src/combinatorics/composition.lean

Created src/combinatorics/partition.lean

added theorem partition.count_of_sums_of_ne_zero

added theorem partition.count_of_sums_zero

added def partition.distincts

added def partition.indiscrete_partition

added def partition.odd_distincts

added def partition.odds

added def partition.of_composition

added theorem partition.of_composition_surj

added def partition.of_multiset

added def partition.of_sums

added structure partition