OAI/RepresentationTheory/Saxl/PathAlternation.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Saxl.PathLayer.tag line 13
  2. def OAI.Saxl.PathLayer.base line 15
  3. def OAI.Saxl.PathLayer.rowAlt line 17
  4. def OAI.Saxl.PathLayer.appendPair line 20
  5. lemma OAI.Saxl.PathLayer.appendPair_left line 23
  6. lemma OAI.Saxl.PathLayer.appendPair_right line 25
  7. lemma OAI.Saxl.PathLayer.tag_left line 28
  8. lemma OAI.Saxl.PathLayer.tag_right line 30
  9. lemma OAI.Saxl.PathLayer.tag_side line 36
  10. lemma OAI.Saxl.PathLayer.rowGroup_sector line 43
  11. lemma OAI.Saxl.PathLayer.rowAlt_step line 56
  12. def OAI.Saxl.PathLayer.J line 79
  13. lemma OAI.Saxl.PathLayer.pair_alt line 81
  14. lemma OAI.Saxl.PathLayer.rowAlt_zero line 105
  15. lemma OAI.Saxl.PathLayer.rowAlt_formula line 131
  16. def OAI.Saxl.fiberRelabel line 147
  17. lemma OAI.Saxl.altWord_fiber_relabel line 163
  18. lemma OAI.Saxl.altWord_letter_eval line 194
  19. def OAI.Saxl.lowLetter line 214
  20. lemma OAI.Saxl.lowLetter_injective line 217
  21. def OAI.Saxl.bandColumnPathEquiv line 221
  22. lemma OAI.Saxl.bandColumnPath_coordinates line 224
  23. lemma OAI.Saxl.bandRow_path_group line 230
  24. lemma OAI.Saxl.bandColumn_path_group line 240
  25. lemma OAI.Saxl.bandRow_path_base line 250
  26. lemma OAI.Saxl.bandColumn_path_base line 266
  27. lemma OAI.Saxl.bandRow_path_eval line 282
  28. lemma OAI.Saxl.bandColumn_path_eval line 289