permanent_permute_cols — Mathlib

English

Permuting columns does not change the permanent: perm(M.submatrix(σ, id)) = perm(M).

Русский

Перестановка столбцов не меняет перманент: perm(M.submatrix(σ, id)) = perm(M).

LaTeX

$$$\\operatorname{permanent}(M_{\\sigma, id}) = \\operatorname{permanent}(M)$$$

Lean4

/-- Permuting the columns does not change the permanent. -/
theorem permanent_permute_cols (σ : Perm n) (M : Matrix n n R) : (M.submatrix σ id).permanent = M.permanent :=
  (Group.mulLeft_bijective σ).sum_comp fun τ ↦ ∏ i : n, M (τ i) i

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