OAI/GroupTheory/PeriodicGroups/Algebra/MatrixTests.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SourceBurnside.WordAlgebra.Table.wordHom line 13
  2. def OAI.SourceBurnside.WordAlgebra.Table.substitution line 18
  3. lemma OAI.SourceBurnside.WordAlgebra.Table.substitution_word line 38
  4. lemma OAI.SourceBurnside.SourceMachine.MachineHierarchy.simulate_replacement line 50
  5. lemma OAI.SourceBurnside.SourceMachine.MachineHierarchy.simulate_zero line 72
  6. def OAI.SourceBurnside.SourceMachine.MachineHierarchy.substitutionWords line 91
  7. def OAI.SourceBurnside.SourceMachine.MachineHierarchy.embeddingHom line 96
  8. lemma OAI.SourceBurnside.SourceMachine.MachineHierarchy.embeddingHom_word line 108
  9. lemma OAI.SourceBurnside.DirectCancellation.maximal_of_uniform line 119
  10. def OAI.SourceBurnside.FiniteTable.Codec.letter line 161
  11. lemma OAI.SourceBurnside.FiniteTable.Codec.eval_letter line 163
  12. lemma OAI.SourceBurnside.FiniteTable.Codec.surviving_of_eval_ne_zero line 172
  13. lemma OAI.SourceBurnside.FiniteTable.Codec.noncolor_isPalette line 177
  14. lemma OAI.SourceBurnside.FiniteTable.Codec.noncolor_headFree line 182
  15. lemma OAI.SourceBurnside.FiniteTable.Codec.eligible_decode line 185
  16. lemma OAI.SourceBurnside.FiniteTable.Codec.letter_commute line 193
  17. lemma OAI.SourceBurnside.FiniteTable.Codec.letter_square line 222
  18. lemma OAI.SourceBurnside.FiniteTable.Codec.long_eligible_interval line 231
  19. def OAI.SourceBurnside.CutReduction.candidates line 248
  20. lemma OAI.SourceBurnside.CutReduction.mem_candidates line 251
  21. def OAI.SourceBurnside.CutReduction.eval line 257
  22. lemma OAI.SourceBurnside.CutReduction.eval_append line 259
  23. lemma OAI.SourceBurnside.CutReduction.length_flatMap line 263
  24. lemma OAI.SourceBurnside.CutReduction.length_le_sum line 272
  25. lemma OAI.SourceBurnside.CutReduction.eval_flatMap line 279
  26. def OAI.SourceBurnside.CutReduction.chunkSum line 287
  27. def OAI.SourceBurnside.CutReduction.letterSum line 290
  28. def OAI.SourceBurnside.CutReduction.join line 293
  29. def OAI.SourceBurnside.CutReduction.language line 296
  30. lemma OAI.SourceBurnside.CutReduction.mem_language line 301
  31. lemma OAI.SourceBurnside.CutReduction.join_injective line 310
  32. theorem OAI.SourceBurnside.CutReduction.letterSum_eq_language line 328
  33. lemma OAI.SourceBurnside.CutReduction.slice_eq_chunk line 365
  34. theorem OAI.SourceBurnside.CutReduction.eventually_letterSum_zero line 400
  35. def OAI.SourceBurnside.MatrixTests.tensor line 450
  36. lemma OAI.SourceBurnside.MatrixTests.tensor_zero line 452
  37. lemma OAI.SourceBurnside.MatrixTests.tensor_one line 454
  38. lemma OAI.SourceBurnside.MatrixTests.tensor_mul line 458
  39. lemma OAI.SourceBurnside.MatrixTests.eval_tensor line 465
  40. def OAI.SourceBurnside.MatrixTests.letterSum line 474
  41. def OAI.SourceBurnside.MatrixTests.chunkSum line 478
  42. lemma OAI.SourceBurnside.MatrixTests.eval_flatMap line 481
  43. lemma OAI.SourceBurnside.MatrixTests.chunkSum_entry line 490
  44. lemma OAI.SourceBurnside.MatrixTests.direct_vanish line 506
  45. lemma OAI.SourceBurnside.CutReduction.letterSum_eq_ofFn line 526
  46. lemma OAI.SourceBurnside.MatrixTests.tensor_left_zero line 549
  47. lemma OAI.SourceBurnside.MatrixTests.tensor_sum line 551
  48. lemma OAI.SourceBurnside.MatrixTests.bounded_list_injective line 556
  49. lemma OAI.SourceBurnside.MatrixTests.chunkSum_eq_sequences line 565
  50. lemma OAI.SourceBurnside.MatrixTests.sum_wordCoefficient_tensor line 581
  51. lemma OAI.SourceBurnside.MatrixTests.automaton_block line 604
  52. lemma OAI.SourceBurnside.MatrixTests.reindex_tensor line 619
  53. lemma OAI.SourceBurnside.MatrixTests.reindex_chunkSum line 622
  54. lemma OAI.SourceBurnside.MatrixTests.direct_vanish_finite line 626