permanent_eq_elem_of_card_eq_one — Mathlib

English

If card n = 1, then permanent(A) = A_{kk} for any k ∈ n.

Русский

Если кардинал множества n равен 1, то permanent(A) = A_{kk} для любого k ∈ n.

LaTeX

$$$\\operatorname{card}(n) = 1 \\Rightarrow \\forall k, \\operatorname{permanent}(A) = A_{kk}$$$

Lean4

theorem permanent_eq_elem_of_card_eq_one {A : Matrix n n R} (h : card n = 1) (k : n) : permanent A = A k k :=
  haveI : Subsingleton n := card_le_one_iff_subsingleton.mp h.le
  permanent_eq_elem_of_subsingleton _ _

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