adjp_apply — Mathlib

English

The (i,j)-entry of adjp equals the stated sign-restricted sum, i.e., adjp_{ij} is the appropriate signed sum over permutations sending j to i.

Русский

Элемент(adj p)_{ij} равен заданной знаковой сумме по перестановкам, отправляющим j в i.

LaTeX

$$$\\operatorname{adjp}_{ij} = \\sum_{\\sigma\\in (\\mathrm{ofSign} s).filter(\\sigma(j)=i)} \\prod_{k\\ne j} A_{k,\\sigma(k)}$$$

Lean4

theorem adjp_apply (i j : n) : adjp s A i j = ∑ σ ∈ (ofSign s).filter (· j = i), ∏ k ∈ { j }ᶜ, A k (σ k) :=
  rfl

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