get_rowLens — Mathlib

English

For μ and i with i less than the length of rowLens, rowLens[i] = rowLen(i).

Русский

Для μ и i, где i меньше длины rowLens, выполняется rowLens[i] = rowLen(i).

LaTeX

$$$$ \forall \mu,i\ (i < |\mu.rowLens|) \Rightarrow \mu.rowLens[i] = \mu.rowLen(i). $$$$

Lean4

@[simp]
theorem get_rowLens {μ : YoungDiagram} {i : Nat} {h : i < μ.rowLens.length} : μ.rowLens[i] = μ.rowLen i := by
  simp only [rowLens, List.getElem_range, List.getElem_map]

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