OAI/GroupTheory/PolycyclicRecognition/Geometry/NilpotentExponentialSurjective.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Surjectivity of the nilpotent exponential from finite BCH

Local regularity gives a neighborhood in the exponential image. The binary BCH formula makes that image a subgroup, so connectedness gives surjectivity. No global exponential chart is assumed.

  1. theorem OAI.PolycyclicRecognition.range_exponential_mem_nhds_of_basis_formula line 24
  2. theorem OAI.PolycyclicRecognition.exponential_surjective_of_nilpotent_dynkin line 50