OAI/Combinatorics/SumProduct/Alignment/CubeFaces01.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubeFaces.face line 22
  2. lemma OAI.CubeFaces.face_apply line 27
  3. lemma OAI.CubeFaces.face_commutator line 30
  4. def OAI.CubeFaces.cube line 38
  5. lemma OAI.CubeFaces.face_mem_cube line 41
  6. def OAI.CubeFaces.upper line 49
  7. lemma OAI.CubeFaces.upper_face line 54
  8. lemma OAI.CubeFaces.map_upper_cube line 60
  9. lemma OAI.CubeFaces.upper_face_apply line 66
  10. lemma OAI.CubeFaces.face_upper_commutator_mem line 70
  11. lemma OAI.CubeFaces.cube_le_normalizer_upper line 84
  12. lemma OAI.CubeFaces.cube_insert_le line 116
  13. lemma OAI.CubeFaces.cube_decompose line 141
  14. def OAI.CubeFaces.evaluation line 151
  15. lemma OAI.CubeFaces.cube_insert_irrelevant line 156
  16. lemma OAI.CubeFaces.cube_eval_mem line 173
  17. lemma OAI.CubeFaces.cube_shift_le line 185
  18. lemma OAI.CubeFaces.cube_restrict line 191
  19. lemma OAI.CubeFaces.cube_normalizes line 201
  20. def OAI.CubeFaces.commModulo line 232
  21. lemma OAI.CubeFaces.face_cube_commutator_mem line 253
  22. lemma OAI.CubeFaces.cube_commutator_mem line 271
  23. lemma OAI.CubeFaces.cube_mono line 286
  24. lemma OAI.CubeFaces.upper_cube_mem line 291