diag_insert

Mathlib.Data.Finset.Prod

URI: https://scilib.ai/kg/mathlib#Finset.diag_insert

English

Inserting an element a into S shifts the diagonal to include (a,a) and the rest of diag(S).

Русский

Вставка элемента a в S добавляет (a,a) к диагонали, оставаясь диагональю S.

LaTeX

$$$\\mathrm{diag}(\\mathrm{insert}\\ a\\ s) = \\mathrm{insert} (a,a)\\ s.\\mathrm{diag}$$$

Lean4

theorem diag_insert : (insert a s).diag = insert (a, a) s.diag := by grind

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

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

Разделы

Аффилиация

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