permanent_permute_rows — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- Permuting the rows does not change the permanent. -/
theorem permanent_permute_rows (σ : Perm n) (M : Matrix n n R) : (M.submatrix id σ).permanent = M.permanent := by
  rw [← permanent_transpose, transpose_submatrix, permanent_permute_cols, permanent_transpose]

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