OAI/GroupTheory/PeriodicGroups/Algebra/WordAlgebra.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SourceBurnside.WordAlgebra.Word line 13
  2. abbrev OAI.SourceBurnside.WordAlgebra.Polynomial line 14
  3. structure OAI.SourceBurnside.WordAlgebra.Table line 16
  4. def OAI.SourceBurnside.WordAlgebra.monomial line 22
  5. theorem OAI.SourceBurnside.WordAlgebra.monomial_one line 24
  6. theorem OAI.SourceBurnside.WordAlgebra.monomial_mul line 25
  7. abbrev OAI.SourceBurnside.WordAlgebra.Table.Reach line 33
  8. def OAI.SourceBurnside.WordAlgebra.Table.Vanishes line 35
  9. lemma OAI.SourceBurnside.WordAlgebra.Table.reach_context line 38
  10. lemma OAI.SourceBurnside.WordAlgebra.Table.vanishes_of_reach line 43
  11. def OAI.SourceBurnside.WordAlgebra.Table.relations line 48
  12. abbrev OAI.SourceBurnside.WordAlgebra.Table.ideal line 52
  13. abbrev OAI.SourceBurnside.WordAlgebra.Table.Algebra line 54
  14. abbrev OAI.SourceBurnside.WordAlgebra.Table.quotient line 56
  15. def OAI.SourceBurnside.WordAlgebra.Table.word line 59
  16. theorem OAI.SourceBurnside.WordAlgebra.Table.word_one line 61
  17. theorem OAI.SourceBurnside.WordAlgebra.Table.word_mul line 63
  18. lemma OAI.SourceBurnside.WordAlgebra.Table.word_rep line 67
  19. lemma OAI.SourceBurnside.WordAlgebra.Table.word_reach line 72
  20. lemma OAI.SourceBurnside.WordAlgebra.Table.word_zero line 83
  21. lemma OAI.SourceBurnside.WordAlgebra.Table.word_eq_zero_of_vanishes line 87
  22. def OAI.SourceBurnside.WordAlgebra.Table.detect line 91
  23. lemma OAI.SourceBurnside.WordAlgebra.Table.detect_single line 97
  24. lemma OAI.SourceBurnside.WordAlgebra.Table.detect_self line 105
  25. lemma OAI.SourceBurnside.WordAlgebra.Table.detect_eq_of_reach line 108
  26. def OAI.SourceBurnside.WordAlgebra.Table.annihilator line 117
  27. lemma OAI.SourceBurnside.WordAlgebra.Table.mem_annihilator line 125
  28. lemma OAI.SourceBurnside.WordAlgebra.Table.relation_in_annihilator line 128
  29. lemma OAI.SourceBurnside.WordAlgebra.Table.ideal_le_annihilator line 151
  30. theorem OAI.SourceBurnside.WordAlgebra.Table.word_ne_zero line 155
  31. theorem OAI.SourceBurnside.WordAlgebra.Table.word_eq_zero_iff line 163
  32. theorem OAI.SourceBurnside.WordAlgebra.Table.word_eq_word_iff line 167
  33. def OAI.SourceBurnside.WordAlgebra.Table.Homogeneous line 188
  34. lemma OAI.SourceBurnside.WordAlgebra.Table.length_eq_of_reach line 190
  35. lemma OAI.SourceBurnside.WordAlgebra.Table.not_vanishes_one line 199
  36. theorem OAI.SourceBurnside.WordAlgebra.Table.nontrivial_algebra line 207
  37. theorem OAI.SourceBurnside.WordAlgebra.Table.infinite_algebra line 213
  38. lemma OAI.SourceBurnside.FiniteTable.Codec.step_context line 236
  39. lemma OAI.SourceBurnside.FiniteTable.Codec.reach_context line 240
  40. lemma OAI.SourceBurnside.FiniteTable.Codec.reach_symm line 245
  41. def OAI.SourceBurnside.FiniteTable.Codec.algebraTable line 250
  42. def OAI.SourceBurnside.FiniteTable.Codec.reachCon line 253
  43. lemma OAI.SourceBurnside.FiniteTable.Codec.reach_iff_table line 264
  44. lemma OAI.SourceBurnside.FiniteTable.Codec.survives_iff_not_vanishes line 283
  45. lemma OAI.SourceBurnside.FiniteTable.Codec.algebraTable_homogeneous line 291
  46. def OAI.SourceBurnside.SourceMachine.MachineHierarchy.table line 299
  47. abbrev OAI.SourceBurnside.SourceMachine.MachineHierarchy.Algebra line 302
  48. theorem OAI.SourceBurnside.SourceMachine.MachineHierarchy.infinite_algebra line 304
  49. def OAI.SourceBurnside.Cancellation.alternatingSum line 320
  50. theorem OAI.SourceBurnside.Cancellation.alternating_eq_zero_of_card_lt line 324
  51. lemma OAI.SourceBurnside.Cancellation.sign_smul_matrix line 334
  52. theorem OAI.SourceBurnside.Cancellation.alternatingSum_eq_zero line 344
  53. def OAI.SourceBurnside.Cancellation.chunkWeight line 366
  54. lemma OAI.SourceBurnside.Cancellation.chunkWeight_append line 370
  55. structure OAI.SourceBurnside.Cancellation.Packet line 374
  56. def OAI.SourceBurnside.Cancellation.Packet.join line 379
  57. def OAI.SourceBurnside.Cancellation.Packet.key line 381
  58. lemma OAI.SourceBurnside.Cancellation.perm_of_key_eq line 384
  59. lemma OAI.SourceBurnside.Cancellation.packet_perm_exists line 391
  60. lemma OAI.SourceBurnside.Cancellation.packet_perm_injective line 419
  61. lemma OAI.SourceBurnside.Cancellation.sum_packet_permutations line 427
  62. def OAI.SourceBurnside.Cancellation.Packet.reorder line 433
  63. lemma OAI.SourceBurnside.Cancellation.Packet.reorder_injective line 436
  64. lemma OAI.SourceBurnside.Cancellation.Packet.reorder_one line 442
  65. lemma OAI.SourceBurnside.Cancellation.sum_reorder_weight line 445
  66. theorem OAI.SourceBurnside.Cancellation.packet_cancellation line 452