Documentation

Mathlib.LinearAlgebra.Matrix.Permanent

Permanent of a matrix #

This file defines the permanent of a matrix, Matrix.permanent, and some of its properties.

Main definitions #

source
def Matrix.permanent {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} [CommSemiring R] (M : Matrix n n R) :
R

The permanent of a square matrix defined as a sum over all permutations. This is analogous to the determinant but without alternating signs.

Equations
source
@[simp]
theorem Matrix.permanent_diagonal {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} [CommSemiring R] {d : n → R} :
(diagonal d).permanent = ∏ i : n, d i
source
@[simp]
theorem Matrix.permanent_zero {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} [CommSemiring R] [Nonempty n] :
permanent 0 = 0
source
@[simp]
theorem Matrix.permanent_one {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} [CommSemiring R] :
permanent 1 = 1
source
theorem Matrix.permanent_isEmpty {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} [CommSemiring R] [IsEmpty n] {A : Matrix n n R} :
A.permanent = 1
source
theorem Matrix.permanent_eq_one_of_card_eq_zero {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} [CommSemiring R] {A : Matrix n n R} (h : Fintype.card n = 0) :
A.permanent = 1
source
@[simp]
theorem Matrix.permanent_unique {R : Type u_2} [CommSemiring R] {n : Type u_3} [Unique n] [DecidableEq n] [Fintype n] (A : Matrix n n R) :
A.permanent = A default default

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.

source
theorem Matrix.permanent_eq_elem_of_subsingleton {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} [CommSemiring R] [Subsingleton n] (A : Matrix n n R) (k : n) :
A.permanent = A k k
source
theorem Matrix.permanent_eq_elem_of_card_eq_one {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} [CommSemiring R] {A : Matrix n n R} (h : Fintype.card n = 1) (k : n) :
A.permanent = A k k
source
@[simp]
theorem Matrix.permanent_transpose {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} [CommSemiring R] (M : Matrix n n R) :
M.transpose.permanent = M.permanent

Transposing a matrix preserves the permanent.

source
theorem Matrix.permanent_permute_cols {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} [CommSemiring R] (σ : Equiv.Perm n) (M : Matrix n n R) :
(M.submatrix (⇑σ) id).permanent = M.permanent

Permuting the columns does not change the permanent.

source
theorem Matrix.permanent_permute_rows {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} [CommSemiring R] (σ : Equiv.Perm n) (M : Matrix n n R) :
(M.submatrix id ⇑σ).permanent = M.permanent

Permuting the rows does not change the permanent.

source
@[simp]
theorem Matrix.permanent_smul {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} [CommSemiring R] (M : Matrix n n R) (c : R) :
(c • M).permanent = c ^ Fintype.card n * M.permanent
source
@[simp]
theorem Matrix.permanent_updateCol_smul {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} [CommSemiring R] (M : Matrix n n R) (j : n) (c : R) (u : n → R) :
(M.updateCol j (c • u)).permanent = c * (M.updateCol j u).permanent
source
@[deprecated Matrix.permanent_updateCol_smul (since := "2024-12-11")]
theorem Matrix.permanent_updateColumn_smul {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} [CommSemiring R] (M : Matrix n n R) (j : n) (c : R) (u : n → R) :
(M.updateCol j (c • u)).permanent = c * (M.updateCol j u).permanent

Alias of Matrix.permanent_updateCol_smul.

source
@[simp]
theorem Matrix.permanent_updateRow_smul {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} [CommSemiring R] (M : Matrix n n R) (j : n) (c : R) (u : n → R) :
(M.updateRow j (c • u)).permanent = c * (M.updateRow j u).permanent