permanent_eq_one_of_card_eq_zero — Mathlib

English

If the cardinality of n is zero, then permanent(A) = 1 for any A.

Русский

Если кардинал множества n равен нулю, то для любой матрицы A выполнено permanent(A) = 1.

LaTeX

$$$\\operatorname{card}(n) = 0 \\Rightarrow \\operatorname{permanent}(A) = 1$$$

Lean4

theorem permanent_eq_one_of_card_eq_zero {A : Matrix n n R} (h : card n = 0) : permanent A = 1 :=
  haveI : IsEmpty n := card_eq_zero_iff.mp h
  permanent_isEmpty

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