permanent_one

Mathlib.LinearAlgebra.Matrix.Permanent

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

English

Let n be finite; the permanent of the identity matrix I_n over a commutative semiring is 1.

Русский

Пусть n — конечное; перманент единичной матрицы I_n над коммутативным полукольцом равен 1.

LaTeX

$$$\\operatorname{permanent}(I_n) = 1$$$

Lean4

@[simp]
theorem permanent_one : permanent (1 : Matrix n n R) = 1 := by rw [← diagonal_one]; simp [-diagonal_one]

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

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

Разделы

Аффилиация

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