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
Instances For
    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
    @[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