OAI/GroupTheory/PolycyclicRecognition/Algebra/PositiveCharacterOrbitSpan.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The positive-relation criterion for a character half-space

  1. def OAI.PolycyclicRecognition.characterNonnegativeMonoid line 13
  2. def OAI.PolycyclicRecognition.representationOrbitSet line 22
  3. def OAI.PolycyclicRecognition.positiveCharacterOrbitSet line 25
  4. theorem OAI.PolycyclicRecognition.positiveCharacterOrbitSpan_stable line 29
  5. theorem OAI.PolycyclicRecognition.positiveCharacterOrbitSpan_eq_top line 48
  6. def OAI.PolycyclicRecognition.characterMonoidRepresentation line 69
  7. theorem OAI.PolycyclicRecognition.finite_characterMonoidModule_of_orbitSpan line 74