OAI/GroupTheory/PolycyclicRecognition/Algebra/RealMatrixSquareLogarithm.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Every squared real linear automorphism has a real logarithm

The semisimple factor uses the conjugation-compatible scalar logarithm of a square. The unipotent factor uses its finite polynomial logarithm.

  1. theorem OAI.PolycyclicRecognition.commute_nilpotentLog_right line 18
  2. theorem OAI.PolycyclicRecognition.analytic_exp_nilpotentLog line 24
  3. theorem OAI.PolycyclicRecognition.real_linear_square_has_log line 28