OAI/GroupTheory/PolycyclicRecognition/Algebra/PolynomialModelDifference.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Polynomial group differences in exponential coordinates

  1. theorem OAI.PolycyclicRecognition.IsPolynomialInBasis.neg line 19
  2. theorem OAI.PolycyclicRecognition.IsPolynomialInBasis.mul line 24
  3. theorem OAI.PolycyclicRecognition.polynomial_model_difference line 34
  4. theorem OAI.PolycyclicRecognition.nilpotent_linear_of_group_difference line 39