OAI/GroupTheory/PolycyclicRecognition/Algebra/NilpotentAutomorphismDifference.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Iterated differences of an automorphism induced by nilpotent conjugation

No commutativity of the invariant subgroup is required. Each successive difference lies one step deeper in the lower central series of the ambient group.

  1. theorem OAI.PolycyclicRecognition.conjugation_difference_iterate_mem line 17
  2. theorem OAI.PolycyclicRecognition.conjugation_difference_iterate_one line 27
  3. theorem OAI.PolycyclicRecognition.automorphism_difference_iterate_map line 32
  4. theorem OAI.PolycyclicRecognition.automorphism_difference_iterate_one line 42