OAI/GroupTheory/PolycyclicRecognition/Algebra/SplitAnnihilator.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Split annihilators and real generalized eigenspaces

The usual finite-dimensional decomposition only needs a split annihilator, rather than an algebraically closed scalar field. Restrictions retain the same annihilator, so the argument also applies to invariant subspaces.

  1. theorem OAI.PolycyclicRecognition.aeval_restrict_apply line 20
  2. theorem OAI.PolycyclicRecognition.aeval_restrict_eq_zero line 35
  3. theorem OAI.PolycyclicRecognition.exists_eigenvalue_of_split_annihilator line 42
  4. theorem OAI.PolycyclicRecognition.iSup_maxGenEigenspace_eq_top_of_split_annihilator line 50