OAI/GroupTheory/PolycyclicRecognition/Algebra/TupleBarPrepend.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Head insertion and contraction in finite-tuple bar coordinates

  1. theorem OAI.PolycyclicRecognition.contractNth_cons_zero line 12
  2. theorem OAI.PolycyclicRecognition.contractNth_cons_succ line 19
  3. def OAI.PolycyclicRecognition.tupleBarPrepend line 27
  4. theorem OAI.PolycyclicRecognition.tupleBarPrepend_single line 31
  5. theorem OAI.PolycyclicRecognition.tupleBarToList_prepend line 35