permanent_isEmpty

Mathlib.LinearAlgebra.Matrix.Permanent

URI: https://scilib.ai/kg/mathlib#Matrix.permanent_isEmpty

English

If n is empty, i.e., there are no indices, the permanent of any n×n matrix is 1.

Русский

Если n пусто, то перманент любой n×n матрицы равен 1.

LaTeX

$$$[IsEmpty\\ n] \\Rightarrow \\operatorname{permanent}(A) = 1 \\,\\text{ for all } A : \\Matrix n n R$$$

Lean4

theorem permanent_isEmpty [IsEmpty n] {A : Matrix n n R} : permanent A = 1 := by simp [permanent]

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

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

Разделы

Аффилиация

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