OAI/GroupTheory/PolycyclicRecognition/Algebra/ConnectedIdealNormality.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Normality of integrated ideals in a connected Lie group

The normalizer contains each exponential one-parameter subgroup, so the basis-generation theorem makes it the whole group. Surjectivity of the ambient exponential is not needed.

  1. theorem OAI.PolycyclicRecognition.normal_of_exponential_ideal_connected line 23
  2. theorem OAI.PolycyclicRecognition.nilpotentIdealNormalityInput_of_connected_exponential line 64