OAI/GroupTheory/PolycyclicRecognition/Algebra/PolynomialOneParameterNilpotent.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Polynomial matrix one-parameter groups have nilpotent derivative

Successive derivatives are left multiplication by successive powers of the initial derivative. A polynomial degree bound therefore forces one power to vanish. This argument uses neither eigenvalues nor triangularization.

  1. def OAI.PolycyclicRecognition.matrixEntryLinear line 22
  2. theorem OAI.PolycyclicRecognition.matrixEntryLinear_apply line 28
  3. theorem OAI.PolycyclicRecognition.polynomial_oneParameter_derivatives line 31
  4. theorem OAI.PolycyclicRecognition.isNilpotent_of_polynomial_oneParameter line 51