OAI/GroupTheory/PolycyclicRecognition/Algebra/PolynomialCoordinateOrbit.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Finite-dimensional coordinate orbits from polynomial multiplication

The coefficients may be arbitrary functions of the right factor. Only the finite polynomial dependence on the left coordinates is needed here.

  1. def OAI.PolycyclicRecognition.coordinateMonomial line 17
  2. def OAI.PolycyclicRecognition.coordinatePolynomialEvaluation line 20
  3. theorem OAI.PolycyclicRecognition.coordinatePolynomialEvaluation_eq_sum line 24
  4. theorem OAI.PolycyclicRecognition.finiteDimensional_coordinateOrbitSpan_of_polynomial line 33