OAI/GroupTheory/PolycyclicRecognition/Algebra/CanonicalNilpotentLogarithm.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A truncation-independent logarithm for unipotent elements

  1. def OAI.PolycyclicRecognition.nilpotentLog line 12
  2. theorem OAI.PolycyclicRecognition.nilpotentLog_eq_of_pow line 15
  3. theorem OAI.PolycyclicRecognition.nilpotentLog_nilpotent line 27
  4. theorem OAI.PolycyclicRecognition.exp_nilpotentLog line 33
  5. theorem OAI.PolycyclicRecognition.nilpotentLog_exp line 38
  6. theorem OAI.PolycyclicRecognition.nilpotentLog_map line 49