coe_copy

Mathlib.Combinatorics.Young.SemistandardTableau

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

← MathLib Explorer

English

The coe of a copied tableau equals the provided entry function entry'.

Русский

Коэф копированной таблицы равен заданной функции записи entry'.

LaTeX

$$$(T.copy(entry')(h))\text{ as a function} = entry'.$$$

Lean4

@[simp]
theorem coe_copy {μ : YoungDiagram} (T : SemistandardYoungTableau μ) (entry' : ℕ → ℕ → ℕ) (h : entry' = T) :
    ⇑(T.copy entry' h) = entry' :=
  rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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