Commit 2023-02-14 05:18 f6e50516

View on Github →

feat Port/Combinatorics.Partition (#2264) port of combinatorics.partition

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/Partition.lean

added theorem Nat.Partition.count_ofSums_of_ne_zero

added theorem Nat.Partition.count_ofSums_zero

added def Nat.Partition.distincts

added def Nat.Partition.indiscretePartition

added def Nat.Partition.oddDistincts

added def Nat.Partition.odds

added def Nat.Partition.ofComposition

added theorem Nat.Partition.ofComposition_surj

added def Nat.Partition.ofMultiset

added def Nat.Partition.ofSums

added structure Nat.Partition