OAI/GroupTheory/PolycyclicRecognition/Algebra/ExteriorScalarDifference.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Commuting scalar-difference operators on an exterior representation

  1. def OAI.PolycyclicRecognition.intertwiningEndForget line 16
  2. def OAI.PolycyclicRecognition.representationEndForget line 25
  3. def OAI.PolycyclicRecognition.exteriorScalarDifference line 29
  4. theorem OAI.PolycyclicRecognition.exteriorScalarDifference_intertwines line 32
  5. def OAI.PolycyclicRecognition.exteriorScalarDifferenceIntertwining line 52
  6. def OAI.PolycyclicRecognition.exteriorScalarDifferenceModule line 57
  7. theorem OAI.PolycyclicRecognition.representationEndForget_difference line 61
  8. theorem OAI.PolycyclicRecognition.exteriorScalarDifferenceModule_commute line 69
  9. theorem OAI.PolycyclicRecognition.polynomialOrbitExterior_scalarDifference line 89