OAI/GroupTheory/PolycyclicRecognition/Algebra/MixedWordBasis.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Finite mixed-word spanning pools for the cone ideals

  1. def OAI.PolycyclicRecognition.CartanWordModel.coneMixedWords line 15
  2. instance OAI.PolycyclicRecognition.CartanWordModel.(instance at line 18) line 18
  3. instance OAI.PolycyclicRecognition.CartanWordModel.(instance at line 23) line 23
  4. def OAI.PolycyclicRecognition.CartanWordModel.coneMixedVector line 26
  5. theorem OAI.PolycyclicRecognition.CartanWordModel.coneWordIdeal_eq_span_finite_mixed line 29
  6. theorem OAI.PolycyclicRecognition.CartanWordModel.coneMixedVector_span line 45
  7. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_cone_mixed_word_basis line 60