product_sdiff_diag

Mathlib.Data.Finset.Prod

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

English

The product set minus the diagonal equals the off-diagonal: S × S \ diag(S) = offDiag(S).

Русский

Произведение множества минус диагональ даёт вне диагонали.

LaTeX

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

Lean4

theorem product_sdiff_diag : s ×ˢ s \ s.diag = s.offDiag := by grind

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

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

Разделы

Аффилиация

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