OAI/GroupTheory/PolycyclicRecognition/Algebra/NilpotentCodimensionOneCriterion.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Nilpotence in a one-dimensional derivation extension

The ideal acts nilpotently on the extension: the first bracket lands in the ideal and all subsequent brackets are adjoint operators of the ideal. Engel's codimension-one criterion then adjoins the nilpotent time operator.

  1. theorem OAI.PolycyclicRecognition.nilpotent_of_codimension_one_restriction line 17
  2. theorem OAI.PolycyclicRecognition.nilpotent_of_split_restriction line 37
  3. theorem OAI.PolycyclicRecognition.nilpotent_derivation_extension line 54