Coefficients of strict alternants

An alternant with a repeated exponent vanishes; the coefficient of a strictly decreasing monomial in a strictly decreasing alternant is the equality indicator — the two facts driving nonnegativity in the Pieri chain.

theorem RS.altDet_eq_zero_of_repeat {k : ℕ} (e : Fin k → ℕ) {i j : Fin k} (hij : i ≠ j) (he : e i = e j) : altDet e = 0

An alternant with a repeated exponent vanishes.

theorem RS.alternant_coeff_strict {k : ℕ} (e w : Fin k → ℕ) (he : ∀ (i j : Fin k), i < j → e j < e i) (hw : ∀ (i j : Fin k), i < j → w j < w i) : (altDet e).coeff (∑ i : Fin k, Finsupp.single i (w i)) = if e = w then 1 else 0

The strict alternant coefficient dichotomy: the coefficient of a strictly decreasing monomial in a strictly decreasing alternant is the equality indicator.