product_sdiff_offDiag

Mathlib.Data.Finset.Prod

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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