OAI/GroupTheory/PolycyclicRecognition/Geometry/PositiveSizeTriangularRepresentation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Positive-size padding for the triangular representation

A trivial one-dimensional summand handles zero-dimensional Lie algebras without a separate group-realization case.

  1. def OAI.PolycyclicRecognition.matrixTrivialSummand line 17
  2. def OAI.PolycyclicRecognition.padTriangularMatrix line 26
  3. theorem OAI.PolycyclicRecognition.padTriangularMatrix_apply line 31
  4. theorem OAI.PolycyclicRecognition.padTriangularMatrix_injective line 37
  5. theorem OAI.PolycyclicRecognition.padTriangularMatrix_upper line 44
  6. theorem OAI.PolycyclicRecognition.padTriangularMatrix_nilpotent line 57
  7. theorem OAI.PolycyclicRecognition.exists_positive_faithful_triangular_representation line 67