copy_eq

Mathlib.Combinatorics.Young.SemistandardTableau

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

← MathLib Explorer

English

If h states that entry' equals the coe of T, then T.copy entry' h equals T.

Русский

Если h задаёт равенство entry' и коe T, то T.copy entry' h = T.

LaTeX

$$$T.copy(entry')(h) = T.$$$

Lean4

theorem copy_eq {μ : YoungDiagram} (T : SemistandardYoungTableau μ) (entry' : ℕ → ℕ → ℕ) (h : entry' = T) :
    T.copy entry' h = T :=
  DFunLike.ext' h

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

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

Разделы

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

Аффилиация

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