OAI/GroupTheory/PolycyclicRecognition/Algebra/RealSemisimpleLogarithm.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A real logarithm of the square of a semisimple unit

  1. def OAI.PolycyclicRecognition.realSemisimpleSquareLog line 12
  2. theorem OAI.PolycyclicRecognition.realSemisimpleSquareLog_complexify line 17
  3. theorem OAI.PolycyclicRecognition.exp_realSemisimpleSquareLog line 27
  4. theorem OAI.PolycyclicRecognition.realSemisimpleSquareLog_commute line 35