OAI/GroupTheory/PolycyclicRecognition/Geometry/ExponentialRangeSubgroup.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The BCH exponential image is a subgroup

Once local exponential coordinates put a neighborhood in the image, connectedness gives surjectivity. No injectivity is needed for this step.

  1. def OAI.PolycyclicRecognition.exponentialRangeSubgroup line 23
  2. theorem OAI.PolycyclicRecognition.exponential_surjective_of_range_mem_nhds line 37