Independence of reduced monomial evaluations

Finite-field interpolation makes evaluation injective on polynomials of degree below the field cardinality in each coordinate. Therefore every family of distinct reduced monomials remains linearly independent as a family of evaluation tables.

theorem Algebraic.MassProduction.HighRate.monomialValuesLinearIndependent {K Coordinate : Type u} {Index : Type u_1} [Field K] [Fintype K] [Fintype Coordinate] (degrees : Index → Coordinate → ℕ) (distinct : Function.Injective degrees) (reduced : ∀ (index : Index) (coordinate : Coordinate), degrees index coordinate < Fintype.card K) : LinearIndependent K fun (index : Index) => monomialValue (degrees index)

Distinct reduced monomials give linearly independent evaluation tables.