Pieri rule for plain alternants

The power-sum p₁ = ∑ l, X l times the plain alternant a_e equals the sum of alternants with one exponent bumped:

`p₁ · a_e = ∑ i, a_{e + δ_i}`.

The proof is a signed-monomial reindexing: expand both sides via det_apply', use the per-term product identity for Function.update, swap/reindex sums via Equiv.sum_comp, and match termwise.

noncomputable def RS.altDet {k : ℕ} (e : Fin k → ℕ) : MvPolynomial (Fin k) ℂ

The plain power alternant of an exponent vector.

Equations

• RS.altDet e = (Matrix.of fun (i j : Fin k) => MvPolynomial.X j ^ e i).det

theorem RS.p1_mul_altDet {k : ℕ} (e : Fin k → ℕ) : (∑ l : Fin k, MvPolynomial.X l) * altDet e = ∑ i : Fin k, altDet (Function.update e i (e i + 1))

The Pieri rule for alternants: multiplying by the first power sum bumps one exponent, summed over which.