OAI/GroupTheory/PolycyclicRecognition/Algebra/CommonEigenvectors.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Finite common eigenspaces and a common eigenvector

Common eigenspaces form an independent family even when the operators do not commute. For commuting operators over an algebraically closed field, a minimal nonzero invariant subspace supplies a common eigenvector.

  1. def OAI.PolycyclicRecognition.commonEigenspace line 21
  2. theorem OAI.PolycyclicRecognition.mem_commonEigenspace line 24
  3. theorem OAI.PolycyclicRecognition.commonEigenspace_independent line 28
  4. theorem OAI.PolycyclicRecognition.finite_commonEigenspaces line 32
  5. theorem OAI.PolycyclicRecognition.exists_commonEigenspace line 36