OAI/GroupTheory/PolycyclicRecognition/Algebra/IntrinsicIdealNormality.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Ideal normality from the intrinsic adjoint flow

Normality of exponential images needs no faithful representation. The actual adjoint action is the exponential of the bracket operator and preserves every Lie ideal.

  1. theorem OAI.PolycyclicRecognition.normal_of_exponential_ideal_intrinsic line 24
  2. theorem OAI.PolycyclicRecognition.nilpotentIdealNormalityInput_of_intrinsic_exponential line 51