OAI/GroupTheory/PolycyclicRecognition/Algebra/FaithfulTruncatedEnveloping.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A faithful nilpotent representation compatible with derivations

A faithful nilpotent representation determines a truncation degree. The resulting finite representation carries the full derivation action, as required for a solvable extension.

  1. theorem OAI.PolycyclicRecognition.exists_faithful_truncated_enveloping line 18
  2. theorem OAI.PolycyclicRecognition.exists_faithful_truncated_semidirect line 26