Def Nat.Partition.ofComposition

Modification history

2023-11-21 01:12

Mathlib/Combinatorics/Partition.lean

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

Modified Nat.Partition.ofComposition View on Github →

2023-02-14 05:18

Mathlib/Combinatorics/Partition.lean

feat Port/Combinatorics.Partition (#2264) …

Added Nat.Partition.ofComposition View on Github →