English
The element s of Sym σ n yields a partition given by its multiplicities: parts are s.1.dedup.map s.1.count, with parts_pos and parts_sum equal to n.
Русский
Элемент s из Sym σ n задаёт разбиение, состоящее из мультипликаций: parts = s.1.dedup.map s.1.count, с properties parts_pos и parts_sum = n.
LaTeX
$$$\mathrm{parts} = s.1.dedup.map s.1.count,\ \mathrm{parts\_pos},\ \mathrm{parts\_sum}=n$$$
Lean4
/-- An element `s` of `Sym σ n` induces a partition given by its multiplicities. -/
def ofSym {n : ℕ} {σ : Type*} (s : Sym σ n) [DecidableEq σ] : n.Partition
where
parts := s.1.dedup.map s.1.count
parts_pos := by simp [Multiset.count_pos]
parts_sum := by
change ∑ a ∈ s.1.toFinset, count a s.1 = n
rw [toFinset_sum_count_eq]
exact s.2
