OAI/GroupTheory/PolycyclicRecognition/Algebra/PolynomialIdealExtensionCoordinates.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Extending polynomial exponential coordinates by one dimension

The smaller ideal supplies its polynomial coordinates. The new semidirect model is represented directly from coordinate translates, so no BCH formula on the new model is assumed.

  1. theorem OAI.PolycyclicRecognition.polynomialCoordinates_extend_ideal line 23