permanent_diagonal — Mathlib

English

The permanent of a diagonal matrix equals the product of its diagonal entries.

Русский

Постоянная диагональной матрицы равна произведению её диагональных элементов.

LaTeX

$$$\operatorname{permanent}(\operatorname{diagonal}(d)) = \prod_i d_i$$$

Lean4

@[simp]
theorem permanent_diagonal {d : n → R} : permanent (diagonal d) = ∏ i, d i :=
  by
  refine (sum_eq_single 1 (fun σ _ hσ ↦ ?_) (fun h ↦ (h <| mem_univ _).elim)).trans ?_
  ·
    match not_forall.mp (mt Equiv.ext hσ) with
    | ⟨x, hx⟩ => exact Finset.prod_eq_zero (mem_univ x) (if_neg hx)
  · simp only [Perm.one_apply, diagonal_apply_eq]

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