rowLens — Mathlib

English

rowLens(μ) is the list of row lengths, defined as (List.range(μ.colLen(0))).map(μ.rowLen).

Русский

rowLens(μ) — список длин строк, заданный как (List.range(μ.colLen(0))).map(μ.rowLen).

LaTeX

$$$$ \mathrm{rowLens}(\mu) = \bigl( \mathrm{List.range}(\mu.colLen(0)) \bigr).\mathrm{map}(\mu.rowLen). $$$$

Lean4

/-- List of row lengths of a Young diagram -/
def rowLens (μ : YoungDiagram) : List ℕ :=
  (List.range <| μ.colLen 0).map μ.rowLen

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