permanent_transpose — Mathlib

English

The permanent is invariant under transposition: perm(M^T) = perm(M).

Русский

Перманент сохраняется при транспонировании: perm(M^T) = perm(M).

LaTeX

$$$\\operatorname{permanent}(M^T) = \\operatorname{permanent}(M)$$$

Lean4

/-- Transposing a matrix preserves the permanent. -/
@[simp]
theorem permanent_transpose (M : Matrix n n R) : Mᵀ.permanent = M.permanent :=
  by
  refine sum_bijective _ inv_involutive.bijective _ _ ?_
  intro σ
  apply Fintype.prod_equiv σ
  simp

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