Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-12 08:59 fd7da4ef

View on Github →

refactor(combinatorics/partition): add nat namespace (#9672) partition is now nat.partition

Estimated changes

Modified src/combinatorics/partition.lean

added theorem nat.partition.count_of_sums_of_ne_zero

added theorem nat.partition.count_of_sums_zero

added def nat.partition.distincts

added def nat.partition.indiscrete_partition

added def nat.partition.odd_distincts

added def nat.partition.odds

added def nat.partition.of_composition

added theorem nat.partition.of_composition_surj

added def nat.partition.of_multiset

added def nat.partition.of_sums

added structure nat.partition

deleted theorem partition.count_of_sums_of_ne_zero

deleted theorem partition.count_of_sums_zero

deleted def partition.distincts

deleted def partition.indiscrete_partition

deleted def partition.odd_distincts

deleted def partition.odds

deleted def partition.of_composition

deleted theorem partition.of_composition_surj

deleted def partition.of_multiset

deleted def partition.of_sums

deleted structure partition

Modified src/group_theory/perm/cycle_type.lean

modified def equiv.perm.partition