rowLen_eq_card

Mathlib.Combinatorics.Young.YoungDiagram

URI: https://scilib.ai/kg/mathlib#YoungDiagram.rowLen_eq_card

English

For every μ and i, the i-th row length equals the cardinality of the i-th row.

Русский

Для каждой μ и i длина i-й строки равна кардиналу i-й строки.

LaTeX

$$$$ \mu.rowLen(i) = (\mu.row(i)).card. $$$$

Lean4

theorem rowLen_eq_card (μ : YoungDiagram) {i : ℕ} : μ.rowLen i = (μ.row i).card := by simp [row_eq_prod]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru