OAI/GroupTheory/PolycyclicRecognition/Geometry/TruncatedSemidirectRepresentation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Representing a semidirect extension on the truncated enveloping algebra

  1. def OAI.PolycyclicRecognition.truncatedLeftRepresentation line 20
  2. theorem OAI.PolycyclicRecognition.truncatedLeftRepresentation_apply line 24
  3. theorem OAI.PolycyclicRecognition.truncated_derivation_left_commutator line 27
  4. theorem OAI.PolycyclicRecognition.truncated_left_derivation_commutator line 36
  5. def OAI.PolycyclicRecognition.truncatedSemidirectRepresentation line 43
  6. theorem OAI.PolycyclicRecognition.truncatedEnvelopingDerivation_one line 69
  7. theorem OAI.PolycyclicRecognition.truncatedSemidirectRepresentation_injective line 77
  8. theorem OAI.PolycyclicRecognition.truncatedLeftRepresentation_nilpotent line 107