OAI/GroupTheory/PolycyclicRecognition/Algebra/DynkinFiniteDifference.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Global inverses for nilpotent BCH translations

Axis normalization fixes the linear term. Every other term raises the lower central series, so the finite correction construction applies.

  1. theorem OAI.PolycyclicRecognition.finiteDynkinPolynomial_collinear_eq_linear line 20
  2. theorem OAI.PolycyclicRecognition.finiteDynkinPolynomial_single_eq_linear line 33
  3. theorem OAI.PolycyclicRecognition.binaryDynkinLinearPart line 45
  4. theorem OAI.PolycyclicRecognition.binaryDynkin_raises_difference line 54
  5. theorem OAI.PolycyclicRecognition.bijective_binaryDynkin_translation line 70
  6. theorem OAI.PolycyclicRecognition.binaryDynkin_raises_left_difference line 79