OAI/GroupTheory/PolycyclicRecognition/Algebra/SpectralLogValue.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Scalar values of a compatible spectral logarithm

  1. def OAI.PolycyclicRecognition.spectralLogValue line 11
  2. theorem OAI.PolycyclicRecognition.spectralLogValue_unit line 18
  3. theorem OAI.PolycyclicRecognition.spectralLogValue_mul line 23
  4. theorem OAI.PolycyclicRecognition.spectralLogValue_conjugation line 31
  5. theorem OAI.PolycyclicRecognition.spectralLogValue_conjugation_all line 39
  6. theorem OAI.PolycyclicRecognition.eigenvalue_ne_zero_of_isUnit line 61
  7. def OAI.PolycyclicRecognition.spectralEigenvalue line 66