rowLen_transpose — Mathlib

English

The row length of the transpose equals the column length of the original: μ^T.rowLen(i) = μ.colLen(i).

Русский

Длина строки транспонированной диаграммы равна длине столбца исходной: μ^T.rowLen(i) = μ.colLen(i).

LaTeX

$$$$ \mu^{\top}.rowLen(i) = \mu.colLen(i). $$$$

Lean4

@[simp]
theorem rowLen_transpose (μ : YoungDiagram) (i : ℕ) : μ.transpose.rowLen i = μ.colLen i := by simp [rowLen, colLen]

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