Leibniz expansion of the Jacobi–Trudi determinant

The determinant of jtMat v in row-normal form: a signed sum over permutations of complete homogeneous products, with terms containing a negative degree vanishing.

theorem RS.det_jtMat_expand {k : ℕ} (v : Fin k → ℕ) : (jtMat v).det = ∑ σ : Equiv.Perm (Fin k), ↑↑(Equiv.Perm.sign σ) * ∏ i : Fin k, hSubZ Finset.univ (↑(v i) + ↑↑(σ i) - ↑↑i)

The Leibniz expansion of the Jacobi–Trudi determinant in row-normal form.

theorem RS.jt_term_guard {k : ℕ} (v : Fin k → ℕ) (σ : Equiv.Perm (Fin k)) : ∏ i : Fin k, hSubZ Finset.univ (↑(v i) + ↑↑(σ i) - ↑↑i) = if ∀ (i : Fin k), 0 ≤ ↑(v i) + ↑↑(σ i) - ↑↑i then ∏ i : Fin k, hSub Finset.univ (↑(v i) + ↑↑(σ i) - ↑↑i).toNat else 0

Guarded form: a Leibniz term with all degrees nonnegative is a complete homogeneous product; otherwise it vanishes.

theorem RS.coeff_det_jtMat {k : ℕ} (v : Fin k → ℕ) (w : Fin k →₀ ℕ) : (jtMat v).det.coeff w = ∑ σ : Equiv.Perm (Fin k), ↑↑(Equiv.Perm.sign σ) * if ∀ (i : Fin k), 0 ≤ ↑(v i) + ↑↑(σ i) - ↑↑i then (∏ i : Fin k, hSub Finset.univ (↑(v i) + ↑↑(σ i) - ↑↑i).toNat).coeff w else 0

Coefficient of the Jacobi–Trudi determinant: signed guarded sum of coefficients of complete homogeneous products.