Coefficient extraction from alternants

The coefficient of the diagonal monomial in a power alternant with injective exponents is 1: distinct permutations contribute distinct monomials, and only the identity hits the diagonal.

theorem RS.sum_single_apply {k : ℕ} (c : Fin k → ℕ) (j : Fin k) : (∑ i : Fin k, Finsupp.single i (c i)) j = c j

Evaluation of a sum of single-point Finsupps.

theorem RS.prod_pow_eq_monomial {k : ℕ} (c : Fin k → ℕ) : ∏ i : Fin k, MvPolynomial.X i ^ c i = (MvPolynomial.monomial (∑ i : Fin k, Finsupp.single i (c i))) 1

Products of variable powers are monomials.

theorem RS.alternant_coeff {k : ℕ} (e : Fin k → ℕ) (hinj : Function.Injective e) : (Matrix.of fun (i j : Fin k) => MvPolynomial.X j ^ e i).det.coeff (∑ i : Fin k, Finsupp.single i (e i)) = 1

The diagonal coefficient of a power alternant with injective exponents is 1.