OAI/GroupTheory/FiniteType/SimplexSign.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimplexSign.lastSwap line 28
  2. lemma OAI.SimplexSign.lastSwap_zero line 31
  3. lemma OAI.SimplexSign.lastSwap_succ line 34
  4. def OAI.SimplexSign.reverseLast line 38
  5. lemma OAI.SimplexSign.reverseLast_succ_zero line 41
  6. lemma OAI.SimplexSign.reverseLast_succ_succ line 44
  7. lemma OAI.SimplexSign.simplex_lastSwap line 58
  8. lemma OAI.SimplexSign.class_lastSwap line 81
  9. def OAI.SimplexSign.classStabilizer line 95
  10. lemma OAI.SimplexSign.alternating_le_classStabilizer line 109
  11. lemma OAI.SimplexSign.class_even line 119
  12. lemma OAI.SimplexSign.class_odd line 124
  13. lemma OAI.SimplexSign.class_sign line 136
  14. def OAI.FacePermutation.restrict line 152
  15. lemma OAI.FacePermutation.succAbove_restrict line 156
  16. def OAI.FacePermutation.liftZero line 161
  17. lemma OAI.FacePermutation.liftZero_zero line 164
  18. lemma OAI.FacePermutation.liftZero_succ line 166
  19. lemma OAI.FacePermutation.sign_liftZero line 168
  20. lemma OAI.FacePermutation.decomposition line 171
  21. lemma OAI.FacePermutation.sign_restrict line 179
  22. def OAI.SimplexVertexMaps.vertexMap line 196
  23. lemma OAI.SimplexVertexMaps.vertexMap_id line 199
  24. lemma OAI.SimplexVertexMaps.vertexMap_comp line 204
  25. lemma OAI.SimplexVertexMaps.vertexMap_perm line 210
  26. lemma OAI.SimplexVertexMaps.vertexMap_face line 216
  27. lemma OAI.SimplexVertexMaps.vertexMap_perm_coordinate line 225
  28. lemma OAI.SimplexVertexMaps.vertexMap_perm_doubleBoundary line 230
  29. lemma OAI.SimplexVertexMaps.vertexMap_zero_of_notMem_range line 236