OAI/Analysis/FreeGroupFactor/RankTwoWords.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.FreeGroupFactorMain.RankTwo.SyllableGroups line 21
  2. abbrev OAI.FreeGroupFactorMain.RankTwo.SyllableGroup line 22
  3. abbrev OAI.FreeGroupFactorMain.RankTwo.NW line 23
  4. def OAI.FreeGroupFactorMain.RankTwo.syllable line 25
  5. def OAI.FreeGroupFactorMain.RankTwo.singleWord line 28
  6. theorem OAI.FreeGroupFactorMain.RankTwo.singleWord_prod line 31
  7. theorem OAI.FreeGroupFactorMain.RankTwo.syllable_add line 35
  8. theorem OAI.FreeGroupFactorMain.RankTwo.syllable_neg line 39
  9. theorem OAI.FreeGroupFactorMain.RankTwo.syllable_zero line 43
  10. theorem OAI.FreeGroupFactorMain.RankTwo.neWord_prod_ne_one line 45
  11. def OAI.FreeGroupFactorMain.RankTwo.longBlock line 55
  12. def OAI.FreeGroupFactorMain.RankTwo.PositiveHead line 58
  13. def OAI.FreeGroupFactorMain.RankTwo.NegativeHead line 62
  14. theorem OAI.FreeGroupFactorMain.RankTwo.positiveHead_ne_one line 65
  15. theorem OAI.FreeGroupFactorMain.RankTwo.negativeHead_ne_one line 70
  16. theorem OAI.FreeGroupFactorMain.RankTwo.longBlock_positive line 79
  17. theorem OAI.FreeGroupFactorMain.RankTwo.longBlock_negative line 88
  18. theorem OAI.FreeGroupFactorMain.RankTwo.positive_mul_positive line 95
  19. theorem OAI.FreeGroupFactorMain.RankTwo.negative_mul_negative line 105
  20. theorem OAI.FreeGroupFactorMain.RankTwo.positive_mul_negative line 116
  21. theorem OAI.FreeGroupFactorMain.RankTwo.negative_mul_positive line 126
  22. def OAI.FreeGroupFactorMain.RankTwo.evalLetters line 141
  23. theorem OAI.FreeGroupFactorMain.RankTwo.evalLetters_nil line 145
  24. theorem OAI.FreeGroupFactorMain.RankTwo.evalLetters_cons line 148
  25. theorem OAI.FreeGroupFactorMain.RankTwo.longBlock_head line 151
  26. theorem OAI.FreeGroupFactorMain.RankTwo.longBlock_injective line 172
  27. def OAI.FreeGroupFactorMain.RankTwo.piece line 195
  28. def OAI.FreeGroupFactorMain.RankTwo.segment line 197
  29. theorem OAI.FreeGroupFactorMain.RankTwo.segment_zero line 201
  30. theorem OAI.FreeGroupFactorMain.RankTwo.segment_succ line 202
  31. theorem OAI.FreeGroupFactorMain.RankTwo.segment_one line 205
  32. theorem OAI.FreeGroupFactorMain.RankTwo.segment_append line 207
  33. theorem OAI.FreeGroupFactorMain.RankTwo.segment_cons line 213
  34. def OAI.FreeGroupFactorMain.RankTwo.coreWord line 217
  35. theorem OAI.FreeGroupFactorMain.RankTwo.segment_core line 223
  36. theorem OAI.FreeGroupFactorMain.RankTwo.segment_longBlock line 231
  37. def OAI.FreeGroupFactorMain.RankTwo.cumulative line 238
  38. theorem OAI.FreeGroupFactorMain.RankTwo.cumulative_zero line 242
  39. theorem OAI.FreeGroupFactorMain.RankTwo.cumulative_succ line 243
  40. theorem OAI.FreeGroupFactorMain.RankTwo.map_cumulative line 246
  41. def OAI.FreeGroupFactorMain.RankTwo.finGenerator line 252
  42. def OAI.FreeGroupFactorMain.RankTwo.prefixGenerator line 255
  43. theorem OAI.FreeGroupFactorMain.RankTwo.prefixGenerator_zero line 258
  44. theorem OAI.FreeGroupFactorMain.RankTwo.prefixGenerator_succ line 259
  45. theorem OAI.FreeGroupFactorMain.RankTwo.finGenerator_fin line 262
  46. def OAI.FreeGroupFactorMain.RankTwo.triangularHom line 265
  47. def OAI.FreeGroupFactorMain.RankTwo.differenceHom line 268
  48. theorem OAI.FreeGroupFactorMain.RankTwo.difference_cumulative line 271
  49. theorem OAI.FreeGroupFactorMain.RankTwo.triangularHom_injective line 281
  50. theorem OAI.FreeGroupFactorMain.RankTwo.cumulative_injective line 293
  51. theorem OAI.FreeGroupFactorMain.RankTwo.intervalBlocks_injective line 312
  52. theorem OAI.FreeGroupFactorMain.RankTwo.boundaryPrefixes_injective line 346
  53. theorem OAI.FreeGroupFactorMain.RankTwo.separatedPrefixes_injective line 378
  54. def OAI.FreeGroupFactorMain.RankTwo.runExponent line 399
  55. theorem OAI.FreeGroupFactorMain.RankTwo.runExponent_pos line 401
  56. theorem OAI.FreeGroupFactorMain.RankTwo.runExponent_strictMono line 406
  57. theorem OAI.FreeGroupFactorMain.RankTwo.separatedSetPrefixes_injective line 415
  58. theorem OAI.FreeGroupFactorMain.RankTwo.mk_eq_one_of_restricted_lift line 434
  59. theorem OAI.FreeGroupFactorMain.RankTwo.prefixRelation_of_separated line 467