Named partitions

This file records some partitions of n that are referred to by name. Two of them are the extremes: Nat.Partition.ones n = (1ⁿ), the finest partition, into n parts equal to 1, is the opposite extreme to Mathlib's coarsest partition Nat.Partition.indiscrete n = (n), whose parts are the single part n when n ≠ 0, and none when n = 0. The third is Nat.Partition.singletonSecondRow n = (n+1, 1), the partition of n+2 with two parts whose second part is a single box; it is written at n+2 so that both parts are positive with no hypothesis on n.

It also records TauCeti.parts_equivCast, the transport of a partition along an equality of the number being partitioned: such a transport leaves the parts alone.

theorem TauCeti.parts_equivCast {m l : ℕ} (h : m = l) (p : m.Partition) : ((Equiv.cast ⋯) p).parts = p.parts

Transporting a partition along an equality of the number being partitioned does not change its parts.

def TauCeti.Nat.Partition.ones (n : ℕ) : n.Partition

The partition (1ⁿ) of n into n parts, each equal to 1.

This is the finest partition of n, opposite to Mathlib's coarsest Nat.Partition.indiscrete n, whose parts are the single part n when n ≠ 0, and none when n = 0.

The parts are exposed only through Nat.Partition.ones_parts.

Equations

• TauCeti.Nat.Partition.ones n = Nat.Partition.ofSums n (Multiset.replicate n 1) ⋯

@[simp]

theorem TauCeti.Nat.Partition.ones_parts (n : ℕ) : (ones n).parts = Multiset.replicate n 1

@[simp]

theorem TauCeti.Nat.Partition.prod_map_factorial_indiscrete (n : ℕ) : (Multiset.map Nat.factorial (Nat.Partition.indiscrete n).parts).prod = n.factorial

The product of the factorials of the parts of the coarsest partition (n) is n !.

For n = 0 this is the empty product, and 0! = 1 agrees with it.

def TauCeti.Nat.Partition.singletonSecondRow (n : ℕ) : (n + 2).Partition

The partition (n+1, 1) of n+2: two parts, the second a single box.

This is the shape usually written (n-1, 1) at n; writing it at n+2 keeps both parts positive with no hypothesis on n. It is the unique shape with two rows whose second row is a single box, and the coarsest shape other than Nat.Partition.indiscrete.

The parts are exposed only through Nat.Partition.singletonSecondRow_parts.

Equations

• TauCeti.Nat.Partition.singletonSecondRow n = Nat.Partition.ofSums (n + 2) {n + 1, 1} ⋯

@[simp]

theorem TauCeti.Nat.Partition.singletonSecondRow_parts (n : ℕ) : (singletonSecondRow n).parts = {n + 1, 1}

The parts of (n+1, 1).

theorem TauCeti.Nat.Partition.sort_parts_singletonSecondRow (n : ℕ) : ((singletonSecondRow n).parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2) = [n + 1, 1]

The decreasingly sorted parts of (n+1, 1).