diag_union_offDiag

Mathlib.Data.Finset.Prod

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

English

The diagonal of S together with its off-diagonal equals S × S.

Русский

Объединение диагонали S и вне диагонали S равняется S × S.

LaTeX

$$$\\mathrm{diag}(s) \\cup \\mathrm{offDiag}(s) = s \\times s$$$

Lean4

@[simp]
theorem diag_union_offDiag : s.diag ∪ s.offDiag = s ×ˢ s := by grind

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

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

Разделы

Аффилиация

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