zeros

Mathlib.Combinatorics.Young.SemistandardTableau

URI: https://scilib.ai/kg/mathlib#SemistandardYoungTableau.zeros

English

If a cell (i,j) is not in μ, then T(i,j) = 0.

Русский

Если клетка (i,j) не принадлежит μ, то T(i,j) = 0.

LaTeX

$$$\forall \mu\; T:\mathrm{SemistandardYoungTableau}(\mu),\ (i,j)\notin \mu\Rightarrow T(i,j)=0.$$$

Lean4

theorem zeros {μ : YoungDiagram} (T : SemistandardYoungTableau μ) {i j : ℕ} (not_cell : (i, j) ∉ μ) : T i j = 0 :=
  T.zeros' not_cell

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

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

Разделы

Аффилиация

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