OAI/GroupTheory/PolycyclicRecognition/Geometry/TriangularExponentialKernel.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Positive triangular exponentials and their kernel

A faithful triangular Lie representation exponentiates into the positive triangular group. Nilradical exponentials are unipotent, and a real upper triangular matrix with exponential equal to the identity is zero.

  1. def OAI.PolycyclicRecognition.positiveTriangularExp line 22
  2. theorem OAI.PolycyclicRecognition.positiveTriangularExp_matrix line 30
  3. theorem OAI.PolycyclicRecognition.triangular_nilpotent_exp_unipotent line 34
  4. theorem OAI.PolycyclicRecognition.triangular_exp_eq_one_iff line 44