OAI/GroupTheory/PolycyclicRecognition/Algebra/DerivationEigenvectors.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Products of eigenvectors of an associative derivation

Real eigenvectors span a subalgebra. Thus an algebra generated by such vectors inherits a spanning family of real eigenvectors.

  1. def OAI.PolycyclicRecognition.derivationEigenvectorSpan line 19
  2. theorem OAI.PolycyclicRecognition.derivationEigenvectorSpan_mul line 21
  3. def OAI.PolycyclicRecognition.derivationEigenvectorSubalgebra line 44