OAI/GroupTheory/PolycyclicRecognition/Algebra/ConeIdealInnerAutomorphism.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The ambient nilpotent inner action on the cone ideal

Every ambient adjoint restricts to a nilpotent derivation of the actual ideal. Its finite exponential is a Lie automorphism with determinant one.

  1. def OAI.PolycyclicRecognition.CartanWordModel.coneIdealInnerDerivation line 23
  2. theorem OAI.PolycyclicRecognition.CartanWordModel.coneIdealInnerDerivation_pow_coe line 34
  3. theorem OAI.PolycyclicRecognition.CartanWordModel.coneIdealInnerDerivation_nilpotent line 46
  4. def OAI.PolycyclicRecognition.CartanWordModel.coneIdealInnerAutomorphism line 57
  5. theorem OAI.PolycyclicRecognition.CartanWordModel.coneIdealInnerAutomorphism_det line 63
  6. theorem OAI.PolycyclicRecognition.CartanWordModel.coneIdealInnerAutomorphism_apply line 69
  7. theorem OAI.PolycyclicRecognition.CartanWordModel.coneIdealInnerAutomorphism_letter line 82