OAI/GroupTheory/PolycyclicRecognition/Algebra/LocalGeneratorAccessibility.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Local accessibility from actual generator words

This uses the proved adjoint spanning and inverse function arguments. No accessibility, regularity or affinity theorem is assumed as an input.

  1. theorem OAI.PolycyclicRecognition.reachable_generatorWords_mem_nhds line 29
  2. theorem OAI.PolycyclicRecognition.eq_of_generator_flow_invariance line 66