OAI/GroupTheory/PolycyclicRecognition/Algebra/SolvableRepresentationAnnihilator.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Real split annihilators for the faithful solvable representation

The semisimple derivation preserves word length, while left multiplication raises it. The finite word-length filtration therefore turns the split annihilator of the derivation into one for their sum.

  1. theorem OAI.PolycyclicRecognition.solvableTruncatedRepresentation_split_annihilator line 27
  2. theorem OAI.PolycyclicRecognition.solvableTruncatedRepresentation_genEigenspaces_span line 61