Def Nat.Partition.indiscrete

Modification history

2023-11-21 01:12

Mathlib/Combinatorics/Partition.lean

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

Added Nat.Partition.indiscrete View on Github →