OAI/GroupTheory/PolycyclicRecognition/Algebra/EnvelopingTruncation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The finite word truncation of an enveloping algebra

The ideal is generated by all sufficiently long products of Lie generators. It is invariant under every extended Lie derivation.

  1. def OAI.PolycyclicRecognition.envelopingLongWords line 21
  2. def OAI.PolycyclicRecognition.envelopingTruncationIdeal line 24
  3. theorem OAI.PolycyclicRecognition.longWord_mem_envelopingTruncationIdeal line 27
  4. theorem OAI.PolycyclicRecognition.word_derivation_mem_truncation line 31
  5. theorem OAI.PolycyclicRecognition.envelopingDerivation_preserves_truncation line 55