OAI/GroupTheory/PolycyclicRecognition/Geometry/TriangularRepresentationKernel.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Faithfulness from the real triangular exponential

Once a group homomorphism integrating the faithful triangular Lie representation is constructed, its kernel is trivial. Surjectivity of the ambient exponential is the only global exponential property used here.

  1. theorem OAI.PolycyclicRecognition.triangular_representation_injective line 18