English
If two Sym σ n elements s and s1 are related by an equivalence on the underlying type via e, then their partitions are equal: Nat.Partition.ofSym s = Nat.Partition.ofSym s1 when s and s1 are related by reshaping with e.
Русский
Если два элемента s и s1 из Sym σ n связаны эквивалентностью по основанию через e, то их разбиения совпадают: Nat.Partition.ofSym s = Nat.Partition.ofSym s1.
LaTeX
$$$$ \\text{ofSym }(s) = \\text{ofSym }(s_1) \\quad \\text{if } s =_{{\\text{Sym }}} s_1 \\text{ under } e. $$$$
Lean4
/-- Given a multiset which sums to `n`, construct a partition of `n` with the same multiset, but
without the zeros.
-/
@[simps]
def ofSums (n : ℕ) (l : Multiset ℕ) (hl : l.sum = n) : Partition n
where
parts := l.filter (· ≠ 0)
parts_pos hi := (of_mem_filter hi).bot_lt
parts_sum := by
have lz : (l.filter (· = 0)).sum = 0 := by simp [sum_eq_zero_iff]
rwa [← filter_add_not (· = 0) l, sum_add, lz, zero_add] at hl
