OAI/GroupTheory/PolycyclicRecognition/Algebra/NilpotentIdealDerivation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The nilpotent derivation in a codimension-one decomposition

  1. def OAI.PolycyclicRecognition.LieCodimensionOneData.derivation line 15
  2. theorem OAI.PolycyclicRecognition.LieCodimensionOneData.ideal_nilpotent_module line 24
  3. theorem OAI.PolycyclicRecognition.LieCodimensionOneData.ideal_nilpotent line 29
  4. theorem OAI.PolycyclicRecognition.LieCodimensionOneData.derivation_nilpotent line 33
  5. theorem OAI.PolycyclicRecognition.LieCodimensionOneData.split_lie line 38

    Source documentation

    In the split coordinates the bracket is the semidirect-product bracket.

    theorem split_lie (x y : D.ideal) (s t : ℝ) :
    ⁅D.split (x, s), D.split (y, t)⁆ =
      D.split (⁅x, y⁆ + s • D.derivation y - t • D.derivation x, 0) := by
…