OAI/GroupTheory/PolycyclicRecognition/Algebra/NilpotentCodimensionOne.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Splitting off one dimension from a nilpotent Lie algebra

The kernel of a nonzero character is a smaller nilpotent ideal. Choosing a vector of character one gives the concrete coordinates for the inductive semidirect-product construction.

  1. structure OAI.PolycyclicRecognition.LieCodimensionOneData line 23
  2. def OAI.PolycyclicRecognition.LieCodimensionOneData.ideal line 35
  3. theorem OAI.PolycyclicRecognition.LieCodimensionOneData.ideal_lt_top line 41
  4. theorem OAI.PolycyclicRecognition.LieCodimensionOneData.finrank_ideal_lt line 49
  5. def OAI.PolycyclicRecognition.LieCodimensionOneData.split line 62
  6. theorem OAI.PolycyclicRecognition.exists_nilpotentCodimensionOneData line 84