OAI/GroupTheory/PolycyclicRecognition/Algebra/LocalGeneratorOrbit.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Adjoint generators restricted to an open family of words

Only arbitrarily small prefixes are needed in the spanning proof. This lets the conjugating words stay inside a specified open coordinate neighborhood.

  1. theorem OAI.PolycyclicRecognition.derivative_mem_submodule_of_eventually line 21
  2. def OAI.PolycyclicRecognition.localBilinearOrbitSpan line 30
  3. theorem OAI.PolycyclicRecognition.local_bilinear_generator_mem line 35
  4. theorem OAI.PolycyclicRecognition.local_bilinear_ad_mem line 41
  5. theorem OAI.PolycyclicRecognition.localBilinearOrbitSpan_eq_top line 62
  6. theorem OAI.PolycyclicRecognition.exists_local_bilinearOrbit_basis line 92