OAI/GroupTheory/PolycyclicRecognition/Algebra/UnconditionalNilpotentCoordinates.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Polynomial nilpotent models by dimension induction

At each successor step, the ideal already has polynomial coordinates. A faithful representation of its semidirect extension proves that extension's finite product law, from which its own exponential coordinates are constructed.

  1. theorem OAI.PolycyclicRecognition.polynomialExponentialCoordinates_nilpotent line 19