ofComposition — Mathlib

English

A multiset l of natural numbers induces a partition on its sum by taking its nonzero parts as the parts of the partition.

Русский

Множество с повторениями l чисел Натуральных порождает разбиение суммы l: не нулевые элементы образуют части разбиения.

LaTeX

$$$ \text{ofMultiset}(l) : l.sum\text{ Partitions} $$$

Lean4

/-- A composition induces a partition (just convert the list to a multiset). -/
@[simps]
def ofComposition (n : ℕ) (c : Composition n) : Partition n
    where
  parts := c.blocks
  parts_pos hi := c.blocks_pos hi
  parts_sum := by rw [Multiset.sum_coe, c.blocks_sum]

Похожие утверждения