OAI/GroupTheory/PolycyclicRecognition/Algebra/SolvableFaithfulRepresentation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A faithful representation nilpotent on the canonical nilradical

The representation is obtained from the proved nilshadow and its finite truncated enveloping algebra. Real triangularization is a separate step.

  1. def OAI.PolycyclicRecognition.solvableTruncatedRepresentation line 25
  2. theorem OAI.PolycyclicRecognition.nilshadowWeightDerivation_eq_zero_of_mem_kernel line 30
  3. theorem OAI.PolycyclicRecognition.solvableTruncatedRepresentation_nilpotent line 43
  4. theorem OAI.PolycyclicRecognition.solvableTruncatedRepresentation_injective line 50
  5. theorem OAI.PolycyclicRecognition.exists_faithful_nilradical_matrix_representation line 59