OAI/GroupTheory/PolycyclicRecognition/Geometry/TriangularExponentialInjective.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Global injectivity of the real upper triangular matrix exponential

Its differential is nonsingular at every point, by the real triangular adjoint calculation. Local injectivity at a logarithm, together with the already proved trivial exponential kernel, excludes every other logarithm.

  1. theorem OAI.PolycyclicRecognition.realTriangularAlgebra_exp_injective line 21