Laplace expansion of the permanent

Mathlib proves cofactor expansion of the determinant along the first row and column (Matrix.det_succ_row_zero, Matrix.det_succ_column_zero). This file proves the analogous expansions of the permanent, without signs: for an (n + 1) × (n + 1) matrix A, A.permanent = ∑ j, A 0 j * (A.submatrix Fin.succ j.succAbove).permanent.

Main results

• Matrix.permanent_succ_column_zero: Laplace expansion of the permanent along column 0.
• Matrix.permanent_succ_row_zero: Laplace expansion of the permanent along row 0.

theorem Matrix.permanent_succ_column_zero {R : Type u_1} [CommSemiring R] {n : ℕ} (A : Matrix (Fin (n + 1)) (Fin (n + 1)) R) : A.permanent = ∑ i : Fin (n + 1), A i 0 * (A.submatrix i.succAbove Fin.succ).permanent

Laplace expansion of the permanent along column 0.

theorem Matrix.permanent_succ_row_zero {R : Type u_1} [CommSemiring R] {n : ℕ} (A : Matrix (Fin (n + 1)) (Fin (n + 1)) R) : A.permanent = ∑ j : Fin (n + 1), A 0 j * (A.submatrix Fin.succ j.succAbove).permanent

Laplace expansion of the permanent along row 0.