OAI/GroupTheory/PolycyclicRecognition/Geometry/NilpotentDifferenceDerivative.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Nilpotence detected by iterating a group difference map

  1. theorem OAI.PolycyclicRecognition.nilpotent_fderiv_of_iterate_zero line 14
  2. theorem OAI.PolycyclicRecognition.nilpotent_difference_fderiv line 22