Commit 2023-11-21 01:12 100f5c20

View on Github →

chore(Combinatorics): golf and cleanup partitions (#8517)

Estimated changes

Modified Mathlib/Combinatorics/Partition.lean

added def Nat.Partition.indiscrete

deleted def Nat.Partition.indiscretePartition

added theorem Nat.Partition.indiscretePartition_parts

modified def Nat.Partition.ofComposition

modified def Nat.Partition.ofMultiset

modified def Nat.Partition.ofSums

added theorem Nat.Partition.partition_one_parts

added theorem Nat.Partition.partition_zero_parts