OAI/GroupTheory/PolycyclicRecognition/Algebra/ConjugateCharacterLog.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Conjugation-compatible logarithms after a finite power

Symmetrizing a compatible logarithm doubles its power and makes it respect the involution. This will preserve real forms in the spectral construction.

  1. def OAI.PolycyclicRecognition.conjugateCharacterLog line 15
  2. theorem OAI.PolycyclicRecognition.conjugateCharacterLog_exp line 23
  3. theorem OAI.PolycyclicRecognition.symmetrizedCharacterLog_conjugation line 28
  4. theorem OAI.PolycyclicRecognition.finitelyGenerated_real_character_power_log line 36