OAI/GroupTheory/PolycyclicRecognition/Algebra/ComplexSquareLogarithm.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A conjugation-compatible logarithm of a complex square

This scalar choice avoids a branch obstruction for the real logarithm of the square of a real linear automorphism.

  1. def OAI.PolycyclicRecognition.complexSquareLog line 14
  2. theorem OAI.PolycyclicRecognition.complexSquareLog_conj line 17
  3. theorem OAI.PolycyclicRecognition.exp_complexSquareLog line 24