OAI/GroupTheory/PolycyclicRecognition/Geometry/SpectralLieDerivation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A compatible spectral logarithm is a Lie derivation

The multiplicative relations among eigenvalues are essential: brackets of eigenvectors have the product eigenvalue, so their logarithmic weights add.

  1. theorem OAI.PolycyclicRecognition.semisimple_bilinear_ext line 20
  2. def OAI.PolycyclicRecognition.spectralLieDerivation line 31