OAI/GroupTheory/PolycyclicRecognition/Geometry/ExponentialNormality.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Normality of exponential subgroups

The manifold differential of conjugation relates invariant Lie ideals to normal exponential subgroups.

  1. theorem OAI.PolycyclicRecognition.exponential_subgroup_normal_of_adjoint_invariant line 22
  2. theorem OAI.PolycyclicRecognition.integrated_range_normal_of_adjoint_invariant line 37