English
If n is a singleton, the permanent of any n×n matrix equals its unique diagonal entry.
Русский
Если n одноэлементное множество, перманент любой матрицы n×n равен единственному диагональному элементу.
LaTeX
$$$\\text{If } n \\text{ is singleton, then } \\operatorname{permanent}(A) = A_{ii} \\text{ for the unique } i \\in n$$$
Lean4
/-- If `n` has only one element, the permanent of an `n` by `n` matrix is just that element.
Although `Unique` implies `DecidableEq` and `Fintype`, the instances might
not be syntactically equal. Thus, we need to fill in the args explicitly. -/
@[simp]
theorem permanent_unique {n : Type*} [Unique n] [DecidableEq n] [Fintype n] (A : Matrix n n R) :
permanent A = A default default := by simp [permanent, univ_unique]
