OAI/GroupTheory/PolycyclicRecognition/Algebra/FiniteShiftProductAlgebra.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Independent coordinates detected by finitely many shifted products

The polynomial ring in n variables is integral over the algebra generated by n+1 distinct scalar evaluations of its monic root polynomial. Interpolation recovers the coefficients; every coordinate is a root of that polynomial.

  1. def OAI.PolycyclicRecognition.shiftProduct line 20
  2. def OAI.PolycyclicRecognition.shiftProductAlgebra line 23
  3. theorem OAI.PolycyclicRecognition.rootPolynomial_coeff_mem_shiftProductAlgebra line 27
  4. theorem OAI.PolycyclicRecognition.coordinate_integral_shiftProductAlgebra line 44
  5. theorem OAI.PolycyclicRecognition.shiftProductAlgebra_integral line 61
  6. theorem OAI.PolycyclicRecognition.shiftProductAlgebra_trdeg line 74
  7. theorem OAI.PolycyclicRecognition.shiftProductAlgebra_independent line 84