OAI/GroupTheory/PolycyclicRecognition/Algebra/PolynomialParameterExtension.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Extending lattice identities through a polynomial coordinate parameter

The parameter need not be linear. This permits ordered exponential coordinates whose integral grid parametrizes a nilpotent lattice.

  1. theorem OAI.PolycyclicRecognition.polynomial_mul_of_parameter_grid line 17
  2. theorem OAI.PolycyclicRecognition.polynomial_leftInverse_of_parameter_grid line 50
  3. def OAI.PolycyclicRecognition.polynomialGroupEquivFromParameter line 61