colLen_transpose — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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